src/Tools/IsaPlanner/isand.ML
changeset 29265 5b4247055bd7
parent 26653 60e0cf6bef89
child 29270 0eade173f77e
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 00:08:11 2008 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Tools/IsaPlanner/isand.ML
     1.5 -    ID:		$Id$
     1.6      Author:     Lucas Dixon, University of Edinburgh
     1.7  
     1.8  Natural Deduction tools.
     1.9 @@ -220,7 +219,7 @@
    1.10     with "names" *)
    1.11  fun fix_vars_to_frees_in_terms names ts = 
    1.12      let 
    1.13 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
    1.14 +      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
    1.15        val Ns = List.foldr Term.add_term_names names ts;
    1.16        val (_,renamings) = 
    1.17            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
    1.18 @@ -259,7 +258,7 @@
    1.19        val ctermify = Thm.cterm_of sgn
    1.20        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
    1.21        val prop = (Thm.prop_of th);
    1.22 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
    1.23 +      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars 
    1.24                                                 [] (prop :: tpairs));
    1.25        val cfixes = 
    1.26            map_filter 
    1.27 @@ -360,7 +359,7 @@
    1.28        val sgn = Thm.theory_of_thm th;
    1.29        val ctermify = Thm.cterm_of sgn;
    1.30  
    1.31 -      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
    1.32 +      val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
    1.33        val cfrees = map (ctermify o Free o lookupfree allfrees) vs
    1.34  
    1.35        val sgs = prems_of th;
    1.36 @@ -420,7 +419,7 @@
    1.37      let
    1.38        val t = Term.strip_all_body alledt;
    1.39        val alls = rev (Term.strip_all_vars alledt);
    1.40 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
    1.41 +      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
    1.42        val names = Term.add_term_names (t,varnames);
    1.43        val fvs = map Free 
    1.44                      (Name.variant_list names (map fst alls)
    1.45 @@ -429,7 +428,7 @@
    1.46  
    1.47  fun fix_alls_term i t = 
    1.48      let 
    1.49 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
    1.50 +      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
    1.51        val names = Term.add_term_names (t,varnames);
    1.52        val gt = Logic.get_goal t i;
    1.53        val body = Term.strip_all_body gt;