src/Tools/IsaPlanner/isand.ML
changeset 29270 0eade173f77e
parent 29265 5b4247055bd7
child 30190 479806475f3c
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 18:53:16 2008 +0100
     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 Term.add_term_tfrees [] ts);
     1.8 -      val tvars = List.foldr Term.add_term_tvars [] ts;
     1.9 +      val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
    1.10 +      val tvars = List.foldr OldTerm.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 = Name.variant Ns n in 
    1.14 @@ -212,7 +212,7 @@
    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 (Term.add_term_tfrees (Thm.prop_of th,[]));
    1.19 +      val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
    1.20      in #2 (Thm.varifyT' skiptfrees th) end;
    1.21  
    1.22  (* change schematic/meta vars to fresh free vars, avoiding name clashes 
    1.23 @@ -220,7 +220,7 @@
    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 Term.add_term_names names ts;
    1.28 +      val Ns = List.foldr OldTerm.add_term_names names ts;
    1.29        val (_,renamings) = 
    1.30            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
    1.31                      let val n2 = Name.variant Ns n in
    1.32 @@ -245,7 +245,7 @@
    1.33        val ctypify = Thm.ctyp_of sgn
    1.34        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
    1.35        val prop = (Thm.prop_of th);
    1.36 -      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
    1.37 +      val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
    1.38        val ctyfixes = 
    1.39            map_filter 
    1.40              (fn (v as ((s,i),ty)) => 
    1.41 @@ -420,7 +420,7 @@
    1.42        val t = Term.strip_all_body alledt;
    1.43        val alls = rev (Term.strip_all_vars alledt);
    1.44        val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
    1.45 -      val names = Term.add_term_names (t,varnames);
    1.46 +      val names = OldTerm.add_term_names (t,varnames);
    1.47        val fvs = map Free 
    1.48                      (Name.variant_list names (map fst alls)
    1.49                         ~~ (map snd alls));
    1.50 @@ -429,7 +429,7 @@
    1.51  fun fix_alls_term i t = 
    1.52      let 
    1.53        val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
    1.54 -      val names = Term.add_term_names (t,varnames);
    1.55 +      val names = OldTerm.add_term_names (t,varnames);
    1.56        val gt = Logic.get_goal t i;
    1.57        val body = Term.strip_all_body gt;
    1.58        val alls = rev (Term.strip_all_vars gt);