src/Tools/IsaPlanner/isand.ML

--- a/src/Tools/IsaPlanner/isand.ML	Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Tools/IsaPlanner/isand.ML	Wed Aug 10 20:53:43 2011 +0200
@@ -186,8 +186,8 @@
 (* change type-vars to fresh type frees *)
 fun fix_tvars_to_tfrees_in_terms names ts = 
     let 
-      val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
-      val tvars = List.foldr OldTerm.add_term_tvars [] ts;
+      val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
+      val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
       val (names',renamings) = 
           List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
                          let val n2 = singleton (Name.variant_list Ns) n in 
@@ -212,15 +212,15 @@
 fun unfix_tfrees ns th = 
     let 
       val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
-      val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
+      val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
     in #2 (Thm.varifyT_global' skiptfrees th) end;
 
 (* change schematic/meta vars to fresh free vars, avoiding name clashes 
    with "names" *)
 fun fix_vars_to_frees_in_terms names ts = 
     let 
-      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
-      val Ns = List.foldr OldTerm.add_term_names names ts;
+      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
+      val Ns = List.foldr Misc_Legacy.add_term_names names ts;
       val (_,renamings) = 
           Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
                     let val n2 = singleton (Name.variant_list Ns) n in
@@ -245,7 +245,7 @@
       val ctypify = Thm.ctyp_of sgn
       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       val prop = (Thm.prop_of th);
-      val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
+      val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
       val ctyfixes = 
           map_filter 
             (fn (v as ((s,i),ty)) => 
@@ -258,7 +258,7 @@
       val ctermify = Thm.cterm_of sgn
       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       val prop = (Thm.prop_of th);
-      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars 
+      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars 
                                                [] (prop :: tpairs));
       val cfixes = 
           map_filter 
@@ -359,7 +359,7 @@
       val sgn = Thm.theory_of_thm th;
       val ctermify = Thm.cterm_of sgn;
 
-      val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
+      val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
       val cfrees = map (ctermify o Free o lookupfree allfrees) vs
 
       val sgs = prems_of th;
@@ -419,8 +419,8 @@
     let
       val t = Term.strip_all_body alledt;
       val alls = rev (Term.strip_all_vars alledt);
-      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
-      val names = OldTerm.add_term_names (t,varnames);
+      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
+      val names = Misc_Legacy.add_term_names (t,varnames);
       val fvs = map Free 
                     (Name.variant_list names (map fst alls)
                        ~~ (map snd alls));
@@ -428,8 +428,8 @@
 
 fun fix_alls_term i t = 
     let 
-      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
-      val names = OldTerm.add_term_names (t,varnames);
+      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
+      val names = Misc_Legacy.add_term_names (t,varnames);
       val gt = Logic.get_goal t i;
       val body = Term.strip_all_body gt;
       val alls = rev (Term.strip_all_vars gt);