# HG changeset patch
# User wenzelm
# Date 1230670149 -3600
# Node ID 7ee78cc8ef2c49f55e85e1cb14e3cf6418a00393
# Parent  010b4dd637fe64c67b146e218dabc2f3dd8f3a72
freeze_thaw: canonical Term.add_XXX operations;
varify: regular name context;

diff -r 010b4dd637fe -r 7ee78cc8ef2c src/Pure/proofterm.ML
--- 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