anchor.diff:  
   let __tc (e : env) (t : term) : tac<(term * typ * guard_t)> =
       bind get (fun ps ->
  -    mlog (fun () -> BU.print1 "Tac> __tc(%s)\n" (tts e t)) (fun () ->
  +    mlog (fun () -> BU.print1 "Tac> __tc(%s)\n" (Print.term_to_string t)) (fun () ->
       let e = {e with uvar_subtyping=false} in
       try ret (ps.main_context.type_of e t)
       with | Errors.Err (_, msg)
  
positive.code:         let w =
              match get_uvar_solved g.goal_ctx_uvar with
              | None -> "_"
              | Some t -> Print.term_to_string t
          in
          BU.format3 "%s |- %s : %s"
               (Print.binders_to_string ", " g.goal_ctx_uvar.ctx_uvar_binders)
               w
               (Print.term_to_string g.goal_ctx_uvar.ctx_uvar_typ)
  
  let tacprint  (s:string)       = BU.print1 "TAC>> %s\n" s
  let tacprint1 (s:string) x     = BU.print1 "TAC>> %s\n" (BU.format1 s x)
  
negative.code: let rewrite (h:binder) : tac<unit> = wrap_err "rewrite" <|
      bind (cur_goal ()) (fun goal ->
      let bv, _ = h in
      mlog (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (Print.bv_to_string bv) (Print.term_to_string bv.sort)) (fun _ ->
      match split_env bv (goal_env goal) with
      | None -> fail "binder not found in environment"
      | Some (e0, bvs) -> begin
  