src/Tools/IsaPlanner/isand.ML
changeset 44121 44adaa6db327
parent 43324 2b47822868e4
child 46217 7b19666f0e3d
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -186,8 +186,8 @@
     1.4  (* change type-vars to fresh type frees *)
     1.5  fun fix_tvars_to_tfrees_in_terms names ts = 
     1.6      let 
     1.7 -      val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
     1.8 -      val tvars = List.foldr OldTerm.add_term_tvars [] ts;
     1.9 +      val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
    1.10 +      val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
    1.11        val (names',renamings) = 
    1.12            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
    1.13                           let val n2 = singleton (Name.variant_list Ns) n in 
    1.14 @@ -212,15 +212,15 @@
    1.15  fun unfix_tfrees ns th = 
    1.16      let 
    1.17        val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
    1.18 -      val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
    1.19 +      val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
    1.20      in #2 (Thm.varifyT_global' skiptfrees th) end;
    1.21  
    1.22  (* change schematic/meta vars to fresh free vars, avoiding name clashes 
    1.23     with "names" *)
    1.24  fun fix_vars_to_frees_in_terms names ts = 
    1.25      let 
    1.26 -      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
    1.27 -      val Ns = List.foldr OldTerm.add_term_names names ts;
    1.28 +      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
    1.29 +      val Ns = List.foldr Misc_Legacy.add_term_names names ts;
    1.30        val (_,renamings) = 
    1.31            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
    1.32                      let val n2 = singleton (Name.variant_list Ns) n in
    1.33 @@ -245,7 +245,7 @@
    1.34        val ctypify = Thm.ctyp_of sgn
    1.35        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
    1.36        val prop = (Thm.prop_of th);
    1.37 -      val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
    1.38 +      val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
    1.39        val ctyfixes = 
    1.40            map_filter 
    1.41              (fn (v as ((s,i),ty)) => 
    1.42 @@ -258,7 +258,7 @@
    1.43        val ctermify = Thm.cterm_of sgn
    1.44        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
    1.45        val prop = (Thm.prop_of th);
    1.46 -      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars 
    1.47 +      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars 
    1.48                                                 [] (prop :: tpairs));
    1.49        val cfixes = 
    1.50            map_filter 
    1.51 @@ -359,7 +359,7 @@
    1.52        val sgn = Thm.theory_of_thm th;
    1.53        val ctermify = Thm.cterm_of sgn;
    1.54  
    1.55 -      val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
    1.56 +      val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
    1.57        val cfrees = map (ctermify o Free o lookupfree allfrees) vs
    1.58  
    1.59        val sgs = prems_of th;
    1.60 @@ -419,8 +419,8 @@
    1.61      let
    1.62        val t = Term.strip_all_body alledt;
    1.63        val alls = rev (Term.strip_all_vars alledt);
    1.64 -      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
    1.65 -      val names = OldTerm.add_term_names (t,varnames);
    1.66 +      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
    1.67 +      val names = Misc_Legacy.add_term_names (t,varnames);
    1.68        val fvs = map Free 
    1.69                      (Name.variant_list names (map fst alls)
    1.70                         ~~ (map snd alls));
    1.71 @@ -428,8 +428,8 @@
    1.72  
    1.73  fun fix_alls_term i t = 
    1.74      let 
    1.75 -      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
    1.76 -      val names = OldTerm.add_term_names (t,varnames);
    1.77 +      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
    1.78 +      val names = Misc_Legacy.add_term_names (t,varnames);
    1.79        val gt = Logic.get_goal t i;
    1.80        val body = Term.strip_all_body gt;
    1.81        val alls = rev (Term.strip_all_vars gt);