anchor.diff:  
               | _ -> e, t, Env.trivial_guard
          end
  +  end
   
   (**************************************************************************************)
   (* Generalizing types *)
  
positive.code:                   | _, (x, Some (Meta tau))::rest ->
                        let t = SS.subst subst x.sort in
                        let v, _, g = new_implicit_var "Instantiation of meta argument" e.pos env t in
                        let mark_meta_implicits tau g =
                            { g with implicits =
                                List.map (fun imp -> { imp with imp_meta = Some (env, tau) }) g.implicits } in
  
negative.code:   let torig = SS.compress t in
    if not env.instantiate_imp
    then e, torig, Env.trivial_guard
    else begin
         if Env.debug env Options.High then
           BU.print2 "maybe_instantiate: starting check for (%s) of type (%s)\n"
                   (Print.term_to_string e) (Print.term_to_string t);
         let number_of_implicits t =
              let formals, _ = U.arrow_formals t in
              let n_implicits =
              match formals |> BU.prefix_until (fun (_, imp) -> imp=None || imp=Some Equality) with
  