# HG changeset patch
# User wenzelm
# Date 1312998341 -7200
# Node ID 88a5a8f44d1513b9c61e0f26eb68dfe08f1b4897
# Parent  c70257b4cb7e29945fccc912cd22159496823ebf
avoid OldTerm operations -- with subtle changes of semantics;

diff -r c70257b4cb7e -r 88a5a8f44d15 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Aug 10 19:21:28 2011 +0200
+++ b/src/Pure/drule.ML	Wed Aug 10 19:45:41 2011 +0200
@@ -302,20 +302,18 @@
 
 
 (*Convert all Vars in a theorem to Frees.  Also return a function for
-  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
-  Similar code in type/freeze_thaw*)
+  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
 
 fun legacy_freeze_thaw_robust th =
  let val fth = Thm.legacy_freezeT th
      val thy = Thm.theory_of_thm fth
-     val {prop, tpairs, ...} = rep_thm fth
  in
-   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+   case Thm.fold_terms Term.add_vars fth [] of
        [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
-         let fun newName (Var(ix,_)) = (ix, legacy_gensym (string_of_indexname ix))
+         let fun newName (ix,_) = (ix, legacy_gensym (string_of_indexname ix))
              val alist = map newName vars
-             fun mk_inst (Var(v,T)) =
+             fun mk_inst (v,T) =
                  (cterm_of thy (Var(v,T)),
                   cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
              val insts = map mk_inst vars
@@ -330,17 +328,16 @@
 fun legacy_freeze_thaw th =
  let val fth = Thm.legacy_freezeT th
      val thy = Thm.theory_of_thm fth
-     val {prop, tpairs, ...} = rep_thm fth
  in
-   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+   case Thm.fold_terms Term.add_vars fth [] of
        [] => (fth, fn x => x)
      | vars =>
-         let fun newName (Var(ix,_), (pairs,used)) =
+         let fun newName (ix, _) (pairs, used) =
                    let val v = singleton (Name.variant_list used) (string_of_indexname ix)
                    in  ((ix,v)::pairs, v::used)  end;
-             val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
-               (prop :: Thm.terms_of_tpairs tpairs, [])) vars
-             fun mk_inst (Var(v,T)) =
+             val (alist, _) =
+                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
+             fun mk_inst (v, T) =
                  (cterm_of thy (Var(v,T)),
                   cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
              val insts = map mk_inst vars