anchor.diff:  
   (* lazy string, for error reporting *)
   type lstring = Thunk.t<string>
  +
  +(* Make a thunk for a string, but keep the UF state
  + * so it can be set before calling the function. This is
  + * used since most error messages call term_to_string,
  + * which will resolve uvars and explode if the version is
  + * wrong. *)
  +let mklstr (f : unit -> string) =
  +    let uf = UF.get () in
  +    Thunk.mk (fun () ->
  +        let tx = UF.new_transaction () in
  +        UF.set uf;
  +        let r = f () in
  +        UF.rollback tx;
  +        r)
   
   (* Instantiation of unification variables *)
   type uvi =
  
positive.code:         in
          match quasi_pattern env lhs with
          | None ->
             let msg = Thunk.mk (fun () ->
                          BU.format1 "first_order heuristic cannot solve %s; lhs not a quasi-pattern"
                            (prob_to_string env orig)) in
             giveup_or_defer env orig wl msg
  
negative.code:          in
           let _, occurs_ok, msg = occurs_check u_lhs arrow in
           if not occurs_ok
           then giveup_or_defer env orig wl (mklstr (fun () -> "occurs-check failed: " ^ (Option.get msg)))
           else aux [] [] formals wl
  
  and solve_binders (env:Env.env) (bs1:binders) (bs2:binders) (orig:prob) (wl:worklist)
  