anchor.diff:          let xvars = List.map mkFreeV vars in
           let dapp =  mkApp(ddconstrsym, xvars) in
   
  -        let tok_typing, decls3 = encode_typ_pred' None t env ddtok_tm in
  +        let tok_typing, decls3 = encode_typ_pred None t env ddtok_tm in
   
           let vars', guards', env'', decls_formals, _ = encode_binders (Some fuel_tm) formals env in //NS/CH: used to be s_fuel_tm
           let ty_pred', decls_pred = 
                let xvars = List.map mkFreeV vars' in
                let dapp =  mkApp(ddconstrsym, xvars) in
  -             encode_typ_pred' (Some fuel_tm) t_res env'' dapp in 
  +             encode_typ_pred (Some fuel_tm) t_res env'' dapp in 
           let guard' = Term.mk_and_l guards' in
           let proxy_fresh = match formals with 
               | [] -> []
  
positive.code:               let encoded_res_t, ty_pred, decls3 = 
                     let res_t = Util.compress_typ res_t in 
                     let encoded_res_t, decls = encode_typ_term res_t env' in 
                     encoded_res_t, mk_HasTypeWithFuel None vapp encoded_res_t, decls in
                let typingAx = Term.Assume(mkForall([vapp], vars, mkImp(guard, ty_pred)), Some "free var typing") in
                let g = decls1@decls2@decls3@typingAx::mk_disc_proj_axioms guard encoded_res_t vapp vars in
                g, env
  
negative.code:             | Inr {v=x; sort=t} -> 
                  let x = unmangle x in
                  let xxsym, xx, env' = gen_term_var env x in
                  let guard_x_t, decls' = encode_typ_pred fuel_opt (norm_t env t) env xx in //if we had polarities, we could generate a mkHasTypeZ here in the negative case
                  (xxsym, Term_sort),
                  guard_x_t,
                  env', 
                  decls',
                  Inr x in
          v::vars, g::guards, env, decls@decls', n::names) ([], [], env, [], []) in
  
      List.rev vars,
      List.rev guards,
      env, 
      decls,
      List.rev names
  
  and encode_typ_pred (fuel_opt:option<term>) (t:typ) (env:env_t) (e:term) : term * decls_t = 
      let t = Util.compress_typ t in 
      let t, decls = encode_typ_term t env in
      mk_HasTypeWithFuel fuel_opt e t, decls
  
  and encode_typ_pred' (fuel_opt:option<term>) (t:typ) (env:env_t) (e:term) : term * decls_t = 
      let t = Util.compress_typ t in 
      let t, decls = encode_typ_term t env in
      match fuel_opt with 
          | None -> mk_HasTypeZ e t, decls
          | Some f -> mk_HasTypeFuel f e t, decls
  
  and encode_typ_term (t:typ) (env:env_t) : (term           (* encoding of t, expects t to be in normal form already *)
                                             * decls_t)     (* top-level declarations to be emitted (for shared representations of existentially bound terms *) = 
  