# HG changeset patch
# User wenzelm
# Date 1312996888 -7200
# Node ID c70257b4cb7e29945fccc912cd22159496823ebf
# Parent  5d9821493bc16009983ffbe36d3596b8774347c1
avoid OldTerm operations -- with subtle changes of semantics;

diff -r 5d9821493bc1 -r c70257b4cb7e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Aug 10 16:26:05 2011 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 10 19:21:28 2011 +0200
@@ -674,11 +674,12 @@
 
 local
 
-fun new_name (ix, (pairs,used)) =
+fun new_name ix (pairs, used) =
   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
-  in  ((ix, v) :: pairs, v :: used)  end;
+  in ((ix, v) :: pairs, v :: used) end;
 
-fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
+fun freeze_one alist (ix, sort) =
+  (case AList.lookup (op =) alist ix of
     NONE => TVar (ix, sort)
   | SOME name => TFree (name, sort));
 
@@ -686,15 +687,14 @@
 
 fun legacy_freezeT t prf =
   let
-    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
-    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
-    val (alist, _) = List.foldr new_name ([], used) tvars;
+    val used = Term.add_tfree_names t [];
+    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
   in
     (case alist of
       [] => prf (*nothing to do!*)
     | _ =>
-      let val frzT = map_type_tvar (freeze_one alist)
-      in map_proof_terms (map_types frzT) frzT prf end)
+        let val frzT = map_type_tvar (freeze_one alist)
+        in map_proof_terms (map_types frzT) frzT prf end)
   end;
 
 end;
diff -r 5d9821493bc1 -r c70257b4cb7e src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Aug 10 16:26:05 2011 +0200
+++ b/src/Pure/type.ML	Wed Aug 10 19:21:28 2011 +0200
@@ -358,7 +358,7 @@
 
 local
 
-fun new_name (ix, (pairs, used)) =
+fun new_name ix (pairs, used) =
   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   in ((ix, v) :: pairs, v :: used) end;
 
@@ -374,18 +374,16 @@
 
 fun legacy_freeze_thaw_type T =
   let
-    val used = OldTerm.add_typ_tfree_names (T, [])
-    and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
-    val (alist, _) = List.foldr new_name ([], used) tvars;
+    val used = Term.add_tfree_namesT T [];
+    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvarsT T [])) ([], used);
   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
 
 val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
 
 fun legacy_freeze_thaw t =
   let
-    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
-    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
-    val (alist, _) = List.foldr new_name ([], used) tvars;
+    val used = Term.add_tfree_names t [];
+    val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
   in
     (case alist of
       [] => (t, fn x => x) (*nothing to do!*)