anchor.diff:      fresh:string -> string;
       string_const:string -> term;
       next_id: unit -> int;
  +    mk_unique:string -> string;
   }
   let varops =
       let initial_ctr = 100 in
  
positive.code:     let ffsym, ff = fresh_fvar "f" Fuel_sort in
      let xx_has_type = mk_HasTypeFuel ff xx tapp in
      Term.Assume(mkForall([[xx_has_type]], (xxsym, Term_sort)::(ffsym, Fuel_sort)::vars,
                           mkImp(xx_has_type, mkEq(tapp, mkApp("PreType", [xx])))), Some "pretyping", Some (varops.fresh "@pretyping_"))
  
  let primitive_type_axioms : env -> lident -> string -> term -> list<decl> =
      let xx = ("x", Term_sort) in
  
negative.code:                      | Some t -> t, []
                       | None ->
                          let cvar_sorts = List.map snd cvars in
                          let fsym = varops.mk_unique ("Tm_abs_" ^ (Util.digest_of_string tkey.hash)) in
                          let fdecl = Term.DeclFun(fsym, cvar_sorts, Term_sort, None) in
                          let f = Term.mkApp(fsym, List.map mkFreeV cvars) in
                          let app = mk_Apply f vars in
  