--- a/src/Pure/proofterm.ML Tue Dec 30 21:48:07 2008 +0100
+++ b/src/Pure/proofterm.ML Tue Dec 30 21:49:09 2008 +0100
@@ -545,15 +545,13 @@
let
val (fs, Tfs, vs, Tvs) = fold_proof_terms
(fn t => fn (fs, Tfs, vs, Tvs) =>
- (add_term_frees (t, fs), add_term_tfree_names (t, Tfs),
- add_term_vars (t, vs), add_term_tvar_ixns (t, Tvs)))
+ (Term.add_free_names t fs, Term.add_tfree_names t Tfs,
+ Term.add_var_names t vs, Term.add_tvar_names t Tvs))
(fn T => fn (fs, Tfs, vs, Tvs) =>
- (fs, add_typ_tfree_names (T, Tfs),
- vs, add_typ_ixns (Tvs, T)))
+ (fs, Term.add_tfree_namesT T Tfs,
+ vs, Term.add_tvar_namesT T Tvs))
prf ([], [], [], []);
- val fs' = map (fst o dest_Free) fs;
- val vs' = map (fst o dest_Var) vs;
- val names = vs' ~~ Name.variant_list fs' (map fst vs');
+ val names = vs ~~ Name.variant_list fs (map fst vs);
val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs);
val rnames = map swap names;
val rnames' = map swap names';
@@ -591,8 +589,9 @@
let
val fs = Term.fold_types (Term.fold_atyps
(fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
- val ixns = add_term_tvar_ixns (t, []);
- val fmap = fs ~~ Name.variant_list (map #1 ixns) (map fst fs);
+ val used = Name.context
+ |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
+ val fmap = fs ~~ (#1 (Name.variants (map fst fs) used));
fun thaw (f as (a, S)) =
(case AList.lookup (op =) fmap f of
NONE => TFree f