anchor.diff:      let t0 = Util.compress_typ t in
       match t0.n with 
         | Typ_btvar a -> 
  -        lookup_typ_var env a, [], []
  +        let t, c = lookup_typ_var env a in
  +        t, [c], []
   
         | Typ_const fv -> 
           lookup_free_tvar env fv, [], []
   
  -      | Typ_fun(binders, res) -> (* TODO: add sharing *)
  -        let doit binders (res:comp) =
  -            let tsym, ttm, fsym, f = fresh_vars "funtype" "f" in
  -            let pretype = mk_tester "Typ_fun" (mk_PreType f) in
  -            let t_has_kind = mk_HasKind ttm Term.mk_Kind_type in
  -            let f_hastype_t = mk_HasType f ttm in
  -            let guard, decls = 
  -                if not <| Absyn.Util.is_pure_comp res
  -                then pretype, [] 
  -                else let vars, guards, env', decls, _ = encode_binders None binders env in 
  -                     let app = mk_ApplyE f vars in
  -                     if Util.is_total_comp res
  -                     then let res_pred, decls' = encode_typ_pred' None (Util.comp_result res) env' app in
  -                          let app_pred = mkForall([app], vars, mkImp(mk_and_l guards, res_pred)) in
  -                          mkAnd(pretype, app_pred), decls@decls'
  -                     else pretype, decls in
  -            ttm, [tsym, Term.mkAnd(t_has_kind, mkForall_fuel([f_hastype_t], [fsym], mkImp(f_hastype_t, guard)))], decls in
  -
  -        begin match binders |> Util.prefix_until (function (Inr _, _) -> true | _ -> false) with 
  -            | Some (t_binders, first_v_binder, rest) -> //explicitly curry the type-binders, since partial type-applications arise via unification commonly in ML programs
  -              begin match t_binders with 
  -                | [] -> doit binders res
  -                | _ -> 
  -                  let res = mk_Typ_fun(first_v_binder::rest, res) (Some ktype) t0.pos |> Syntax.mk_Total in
  -                  doit t_binders res
  -             end
  -            | None -> doit binders res 
  -        end
  +      | Typ_fun(binders, res) -> 
  +        (* TODO: sharing; check that currying works properly; handling non-total functions *)
  +        if   Absyn.Util.is_total_comp res
  +        then let vars, cvars, guards, env', decls, _ = encode_binders None binders env in 
  +             let fsym = varops.fresh "f", Term_sort in
  +             let f = mkBoundV fsym in
  +             let app = mk_ApplyE f vars in      
  +             let res_pred, cvars', decls' = encode_typ_pred' None (Util.comp_result res) env' app in
  +
  +             let cvars = exclude_cvars binders (cvars@cvars') in
  +             let cvar_binders = cvar_binders cvars in
  +
  +             let tsym = varops.fresh "Typ_fun" in
  +             let tdecl = Term.DeclFun(tsym, cvar_sorts cvars, Type_sort, None) in
  +             let t = Term.mkApp(tsym, cvar_terms cvars) in
  +             let t_has_kind = mk_HasKind t Term.mk_Kind_type in
  +
  +
  +             let k_assumption = Term.Assume(Term.mkForall([t_has_kind], cvar_binders, t_has_kind), None) in
  +             let f_has_t = mk_HasType f t in
  +             let t_interp = Term.Assume(mkForall_fuel([f_has_t], fsym::cvar_binders, 
  +                                                      mkIff(f_has_t, 
  +                                                            mkAnd(mk_tester "Typ_fun" (mk_PreType f), 
  +                                                                  mkForall([app], vars,  
  +                                                                              mkImp(mk_and_l guards, res_pred))))), 
  +                                       Some (tsym ^ " interpretation")) in 
  +            
  +             t, cvars, decls@decls'@[tdecl; k_assumption; t_interp]              
  +
  +        else let tsym = varops.fresh "funtype" in
  +             let t = Term.mkFreeV(tsym, Type_sort) in
  +             let tdecl = Term.DeclFun(tsym, [], Type_sort, None) in
  +             t, [], [tdecl] (* TODO: At least preserve alpha-equivalence of non-pure function types *)
         
         | Typ_refine _ -> 
           let x, f = match Tc.Normalize.normalize_refinement env.tcenv t0 with 
  
positive.code:     | Binding_tvar  of btvdef * term
      | Binding_fvar  of lident * string * term * option<term> (* free variables, depending on whether or not they are fully applied ...  *)
      | Binding_ftvar of lident * string * term (* ... are mapped either to SMT2 functions, or to nullary term/type tokens *)
     
  type env_t = {bindings:list<binding>;
                tcenv:Env.env;
                warn:bool;
  
negative.code:         | Inr e, _ -> let t, vs, decls' = encode_exp e env in Inr t::tms, vs@ex_vars, decls@decls') ([], [], []) in
      List.rev l, vars, decls
  
  and encode_formula (phi:typ) (env:env_t) : term * closure_vars * decls_t = 
      let t, vars, cvars, decls = encode_formula_with_labels phi env in
      match vars with
          | [] -> t, cvars, decls
          | _ -> failwith "Unexpected labels in formula"
    
  and encode_function_type_as_formula (use_decreasing_pat:bool) (t:typ) (env:env_t) : term * decls_t = 
  