anchor.diff:                                      (U.mk_eq2 (TcTerm.universe_of env typ) typ t ut) opts) (fun _ ->
             focus (
                   bind tau (fun _ ->
  -                log ps (fun () ->
                   // Try to get rid of all the unification lambdas
                   let ut = N.reduce_uvar_solutions env ut in
  -                BU.print2 "Pointwise_rec: succeeded rewriting\n\t%s to\n\t%s\n" (Print.term_to_string t)
  -                                                                                (Print.term_to_string ut));
  -                
  -
  +                log ps (fun () ->
  +                    BU.print2 "Pointwise_rec: succeeded rewriting\n\t%s to\n\t%s\n"
  +                                (Print.term_to_string t)
  +                                (Print.term_to_string ut));
                   ret ut))
  -          )) 
  +          ))
          in
  -       bind (trytac rewrite_eq) (fun x -> 
  +       bind (trytac rewrite_eq) (fun x ->
          match x with
          | None -> ret t
          | Some x -> ret x)
  -       
   
   let pointwise (d : direction) (tau:tac<unit>) : tac<unit> =
       bind get (fun ps ->
  
positive.code:     bind (if d = TopDown
            then f env ({ t with n = tn })
            else ret t) (fun t ->
      let tn = match tn with
               | Tm_app (hd, args) ->
                    let ff = tac_fold_env d f env in
                    bind (ff hd) (fun hd ->
  
negative.code:     in
      // Lemma post is thunked
      let post = U.mk_app post [S.as_arg U.exp_unit] in
      if not (do_unify goal.context (U.mk_squash post) goal.goal_ty)
      then fail3 "Cannot instantiate lemma %s (with postcondition: %s) to match goal (%s)"
                              (N.term_to_string goal.context tm)
                              (N.term_to_string goal.context (U.mk_squash post))
  