moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
authorwenzelm
Wed Dec 31 18:53:16 2008 +0100 (2008-12-31)
changeset 292700eade173f77e
parent 29269 5c25a2012975
child 29271 1d685baea08e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Inductive.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/List.thy
src/HOL/Matrix/cplex/matrixlp.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_case.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/code_unit.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/codegen.ML
src/Pure/drule.ML
src/Pure/old_term.ML
src/Pure/proofterm.ML
src/Pure/term.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 15:30:10 2008 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 18:53:16 2008 +0100
     1.3 @@ -1149,7 +1149,7 @@
     1.4        val t = term_of ct
     1.5        val thy = theory_of_cterm ct
     1.6        val frees = OldTerm.term_frees t
     1.7 -      val freenames = add_term_free_names (t, [])
     1.8 +      val freenames = OldTerm.add_term_free_names (t, [])
     1.9        fun is_old_name n = n mem_string freenames
    1.10        fun name_of (Free (n, _)) = n
    1.11          | name_of _ = ERR "name_of"
    1.12 @@ -1218,7 +1218,7 @@
    1.13                           c = "All" orelse
    1.14                           c = "op -->" orelse
    1.15                           c = "op &" orelse
    1.16 -                         c = "op =")) (Term.term_consts tm)
    1.17 +                         c = "op =")) (OldTerm.term_consts tm)
    1.18  
    1.19  fun match_consts t (* th *) =
    1.20      let
    1.21 @@ -1423,9 +1423,9 @@
    1.22      let
    1.23          val _ = message "INST_TYPE:"
    1.24          val _ = if_debug pth hth
    1.25 -        val tys_before = add_term_tfrees (prop_of th,[])
    1.26 +        val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
    1.27          val th1 = Thm.varifyT th
    1.28 -        val tys_after = add_term_tvars (prop_of th1,[])
    1.29 +        val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
    1.30          val tyinst = map (fn (bef, iS) =>
    1.31                               (case try (Lib.assoc (TFree bef)) lambda of
    1.32                                    SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
    1.33 @@ -2092,7 +2092,7 @@
    1.34              val c = case concl_of th2 of
    1.35                          _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
    1.36                        | _ => raise ERR "new_type_definition" "Bad type definition theorem"
    1.37 -            val tfrees = term_tfrees c
    1.38 +            val tfrees = OldTerm.term_tfrees c
    1.39              val tnames = map fst tfrees
    1.40              val tsyn = mk_syn thy tycname
    1.41              val typ = (tycname,tnames,tsyn)
    1.42 @@ -2178,7 +2178,7 @@
    1.43              val c = case concl_of th2 of
    1.44                          _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
    1.45                        | _ => raise ERR "type_introduction" "Bad type definition theorem"
    1.46 -            val tfrees = term_tfrees c
    1.47 +            val tfrees = OldTerm.term_tfrees c
    1.48              val tnames = sort string_ord (map fst tfrees)
    1.49              val tsyn = mk_syn thy tycname
    1.50              val typ = (tycname,tnames,tsyn)
     2.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
     2.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 18:53:16 2008 +0100
     2.3 @@ -247,8 +247,8 @@
     2.4  
     2.5  fun freeze_thaw_term t =
     2.6      let
     2.7 -        val tvars = term_tvars t
     2.8 -        val tfree_names = add_term_tfree_names(t,[])
     2.9 +        val tvars = OldTerm.term_tvars t
    2.10 +        val tfree_names = OldTerm.add_term_tfree_names(t,[])
    2.11          val (type_inst,_) =
    2.12              Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
    2.13                        let
    2.14 @@ -267,7 +267,7 @@
    2.15    | inst_tfrees thy ((name,U)::rest) thm =
    2.16      let
    2.17          val cU = ctyp_of thy U
    2.18 -        val tfrees = add_term_tfrees (prop_of thm,[])
    2.19 +        val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
    2.20          val (rens, thm') = Thm.varifyT'
    2.21      (remove (op = o apsnd fst) name tfrees) thm
    2.22          val mid =
    2.23 @@ -321,7 +321,7 @@
    2.24                then
    2.25                    let
    2.26                        val cert = cterm_of thy
    2.27 -                      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
    2.28 +                      val v = Free(Name.variant (OldTerm.add_term_free_names(t,[])) "v",xT)
    2.29                        val cv = cert v
    2.30                        val ct = cert t
    2.31                        val th = (assume ct)
    2.32 @@ -384,7 +384,7 @@
    2.33                        Type("fun",[aT,bT]) =>
    2.34                        let
    2.35                            val cert = cterm_of thy
    2.36 -                          val vname = Name.variant (add_term_free_names(t,[])) "v"
    2.37 +                          val vname = Name.variant (OldTerm.add_term_free_names(t,[])) "v"
    2.38                            val v = Free(vname,aT)
    2.39                            val cv = cert v
    2.40                            val ct = cert t
    2.41 @@ -572,8 +572,8 @@
    2.42      fold_rev (fn thm => fn cs =>
    2.43                let
    2.44                    val (lhs,rhs) = Logic.dest_equals (prop_of thm)
    2.45 -                  val ignore_lhs = term_consts lhs \\ term_consts rhs
    2.46 -                  val ignore_rhs = term_consts rhs \\ term_consts lhs
    2.47 +                  val ignore_lhs = OldTerm.term_consts lhs \\ OldTerm.term_consts rhs
    2.48 +                  val ignore_rhs = OldTerm.term_consts rhs \\ OldTerm.term_consts lhs
    2.49                in
    2.50                    fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    2.51                end)
     3.1 --- a/src/HOL/Inductive.thy	Wed Dec 31 15:30:10 2008 +0100
     3.2 +++ b/src/HOL/Inductive.thy	Wed Dec 31 18:53:16 2008 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Inductive.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Markus Wenzel, TU Muenchen
     3.7  *)
     3.8  
     3.9 @@ -363,7 +362,7 @@
    3.10  let
    3.11    fun fun_tr ctxt [cs] =
    3.12      let
    3.13 -      val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
    3.14 +      val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
    3.15        val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
    3.16                   ctxt [x, cs]
    3.17      in lambda x ft end
     4.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 15:30:10 2008 +0100
     4.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 18:53:16 2008 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Library/Efficient_Nat.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
     4.7  *)
     4.8  
     4.9 @@ -170,7 +169,7 @@
    4.10  fun eqn_suc_preproc thy ths =
    4.11    let
    4.12      val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
    4.13 -    fun contains_suc t = member (op =) (term_consts t) @{const_name Suc};
    4.14 +    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
    4.15    in
    4.16      if forall (can dest) ths andalso
    4.17        exists (contains_suc o dest) ths
    4.18 @@ -212,7 +211,7 @@
    4.19      val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
    4.20    in
    4.21      if forall (can (dest o concl_of)) ths andalso
    4.22 -      exists (fn th => member (op =) (foldr add_term_consts
    4.23 +      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
    4.24          [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
    4.25      then remove_suc_clause thy ths else ths
    4.26    end;
     5.1 --- a/src/HOL/List.thy	Wed Dec 31 15:30:10 2008 +0100
     5.2 +++ b/src/HOL/List.thy	Wed Dec 31 18:53:16 2008 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/List.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7  *)
     5.8  
     5.9 @@ -359,7 +358,7 @@
    5.10  
    5.11     fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
    5.12      let
    5.13 -      val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT);
    5.14 +      val x = Free (Name.variant (OldTerm.add_term_free_names (p$e, [])) "x", dummyT);
    5.15        val e = if opti then singl e else e;
    5.16        val case1 = Syntax.const "_case1" $ p $ e;
    5.17        val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
     6.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Dec 31 15:30:10 2008 +0100
     6.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Wed Dec 31 18:53:16 2008 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/Matrix/cplex/matrixlp.ML
     6.5 -    ID:         $Id$
     6.6      Author:     Steven Obua
     6.7  *)
     6.8  
     6.9 @@ -20,7 +19,7 @@
    6.10  fun inst_real thm =
    6.11    let val certT = ctyp_of (Thm.theory_of_thm thm) in
    6.12      standard (Thm.instantiate
    6.13 -      ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    6.14 +      ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
    6.15    end
    6.16  
    6.17  local
    6.18 @@ -58,7 +57,7 @@
    6.19      let
    6.20          val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
    6.21          val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
    6.22 -        val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
    6.23 +        val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
    6.24      in
    6.25          standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
    6.26      end
     7.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 15:30:10 2008 +0100
     7.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 18:53:16 2008 +0100
     7.3 @@ -247,7 +247,7 @@
     7.4  (* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw
     7.5     and thm.instantiate *)
     7.6  fun freeze_thaw t =
     7.7 -  let val used = add_term_names (t, [])
     7.8 +  let val used = OldTerm.add_term_names (t, [])
     7.9            and vars = OldTerm.term_vars t;
    7.10        fun newName (Var(ix,_), (pairs,used)) = 
    7.11            let val v = Name.variant used (string_of_indexname ix)
     8.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 15:30:10 2008 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 18:53:16 2008 +0100
     8.3 @@ -152,7 +152,7 @@
     8.4      val elims = map (atomize_induct ctxt) elims;
     8.5      val monos = InductivePackage.get_monos ctxt;
     8.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     8.7 -    val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
     8.8 +    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
     8.9          [] => ()
    8.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    8.11            commas_quote xs));
    8.12 @@ -199,8 +199,8 @@
    8.13      val ind_sort = if null atomTs then HOLogic.typeS
    8.14        else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
    8.15          ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs);
    8.16 -    val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n";
    8.17 -    val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z";
    8.18 +    val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
    8.19 +    val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
    8.20      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    8.21  
    8.22      val inductive_forall_def' = Drule.instantiate'
    8.23 @@ -411,7 +411,7 @@
    8.24        let
    8.25          val prem :: prems = Logic.strip_imp_prems rule;
    8.26          val concl = Logic.strip_imp_concl rule;
    8.27 -        val used = add_term_free_names (rule, [])
    8.28 +        val used = OldTerm.add_term_free_names (rule, [])
    8.29        in
    8.30          (prem,
    8.31           List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params),
    8.32 @@ -613,7 +613,7 @@
    8.33        [mk_perm_bool_simproc names,
    8.34         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    8.35      val t = Logic.unvarify (concl_of raw_induct);
    8.36 -    val pi = Name.variant (add_term_names (t, [])) "pi";
    8.37 +    val pi = Name.variant (OldTerm.add_term_names (t, [])) "pi";
    8.38      val ps = map (fst o HOLogic.dest_imp)
    8.39        (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
    8.40      fun eqvt_tac pi (intr, vs) st =
     9.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 15:30:10 2008 +0100
     9.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 18:53:16 2008 +0100
     9.3 @@ -158,7 +158,7 @@
     9.4      val elims = map (atomize_induct ctxt) elims;
     9.5      val monos = InductivePackage.get_monos ctxt;
     9.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     9.7 -    val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
     9.8 +    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
     9.9          [] => ()
    9.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    9.11            commas_quote xs));
    9.12 @@ -221,8 +221,8 @@
    9.13      val ind_sort = if null atomTs then HOLogic.typeS
    9.14        else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
    9.15          ("fs_" ^ Sign.base_name a)) atoms);
    9.16 -    val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n";
    9.17 -    val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z";
    9.18 +    val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
    9.19 +    val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
    9.20      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    9.21  
    9.22      val inductive_forall_def' = Drule.instantiate'
    10.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Dec 31 15:30:10 2008 +0100
    10.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Dec 31 18:53:16 2008 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Nominal/nominal_package.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Stefan Berghofer and Christian Urban, TU Muenchen
    10.7  
    10.8  Nominal datatype package for Isabelle/HOL.
    10.9 @@ -1414,7 +1413,7 @@
   10.10  
   10.11      val _ = warning "defining recursion combinator ...";
   10.12  
   10.13 -    val used = foldr add_typ_tfree_names [] recTs;
   10.14 +    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
   10.15  
   10.16      val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used;
   10.17  
    11.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 15:30:10 2008 +0100
    11.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 18:53:16 2008 +0100
    11.3 @@ -123,7 +123,7 @@
    11.4  
    11.5        val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
    11.6  
    11.7 -      val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
    11.8 +      val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
    11.9        val (Pv, Dv, type_insts) =
   11.10            case (Thm.concl_of case_thm) of
   11.11              (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
    12.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 15:30:10 2008 +0100
    12.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 18:53:16 2008 +0100
    12.3 @@ -514,7 +514,7 @@
    12.4                  val (f,args) = S.strip_comb (get_lhs eq)
    12.5                  val (vstrl,_) = S.strip_abs f
    12.6                  val names  =
    12.7 -                  Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
    12.8 +                  Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
    12.9              in get (rst, n+1, (names,n)::L) end
   12.10              handle TERM _ => get (rst, n+1, L)
   12.11                | U.ERR _ => get (rst, n+1, L);
   12.12 @@ -803,7 +803,7 @@
   12.13      (if (is_cong thm) then cong_prover else restrict_prover) ss thm
   12.14      end
   12.15      val ctm = cprop_of th
   12.16 -    val names = add_term_names (term_of ctm, [])
   12.17 +    val names = OldTerm.add_term_names (term_of ctm, [])
   12.18      val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
   12.19        (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
   12.20      val th2 = equal_elim th1 th
    13.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Dec 31 15:30:10 2008 +0100
    13.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Dec 31 18:53:16 2008 +0100
    13.3 @@ -1,7 +1,5 @@
    13.4  (*  Title:      HOL/Tools/TFL/tfl.ML
    13.5 -    ID:         $Id$
    13.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    13.7 -    Copyright   1997  University of Cambridge
    13.8  
    13.9  First part of main module.
   13.10  *)
   13.11 @@ -332,7 +330,7 @@
   13.12       val dummy = map (no_repeat_vars thy) pats
   13.13       val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
   13.14                                map (fn (t,i) => (t,(i,true))) (enumerate R))
   13.15 -     val names = foldr add_term_names [] R
   13.16 +     val names = foldr OldTerm.add_term_names [] R
   13.17       val atype = type_of(hd pats)
   13.18       and aname = Name.variant names "a"
   13.19       val a = Free(aname,atype)
   13.20 @@ -494,7 +492,7 @@
   13.21       val tych = Thry.typecheck thy
   13.22       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   13.23       val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   13.24 -     val R = Free (Name.variant (foldr add_term_names [] eqns) Rname,
   13.25 +     val R = Free (Name.variant (foldr OldTerm.add_term_names [] eqns) Rname,
   13.26                     Rtype)
   13.27       val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
   13.28       val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
   13.29 @@ -692,7 +690,7 @@
   13.30   let val tych = Thry.typecheck thy
   13.31       val ty_info = Thry.induct_info thy
   13.32   in fn pats =>
   13.33 - let val names = foldr add_term_names [] pats
   13.34 + let val names = foldr OldTerm.add_term_names [] pats
   13.35       val T = type_of (hd pats)
   13.36       val aname = Name.variant names "a"
   13.37       val vname = Name.variant (aname::names) "v"
   13.38 @@ -845,7 +843,7 @@
   13.39      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   13.40      val case_thm = complete_cases thy pats
   13.41      val domain = (type_of o hd) pats
   13.42 -    val Pname = Name.variant (foldr (Library.foldr add_term_names)
   13.43 +    val Pname = Name.variant (foldr (Library.foldr OldTerm.add_term_names)
   13.44                                [] (pats::TCsl)) "P"
   13.45      val P = Free(Pname, domain --> HOLogic.boolT)
   13.46      val Sinduct = R.SPEC (tych P) Sinduction
   13.47 @@ -856,7 +854,7 @@
   13.48      val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
   13.49      val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   13.50      val proved_cases = map (prove_case fconst thy) tasks
   13.51 -    val v = Free (Name.variant (foldr add_term_names [] (map concl proved_cases))
   13.52 +    val v = Free (Name.variant (foldr OldTerm.add_term_names [] (map concl proved_cases))
   13.53                      "v",
   13.54                    domain)
   13.55      val vtyped = tych v
    14.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 15:30:10 2008 +0100
    14.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 18:53:16 2008 +0100
    14.3 @@ -112,7 +112,7 @@
    14.4  
    14.5  val is_vartype = can dest_vtype;
    14.6  
    14.7 -val type_vars  = map mk_prim_vartype o typ_tvars
    14.8 +val type_vars  = map mk_prim_vartype o OldTerm.typ_tvars
    14.9  fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
   14.10  
   14.11  val alpha  = mk_vartype "'a"
   14.12 @@ -142,7 +142,7 @@
   14.13  
   14.14  
   14.15  
   14.16 -val type_vars_in_term = map mk_prim_vartype o term_tvars;
   14.17 +val type_vars_in_term = map mk_prim_vartype o OldTerm.term_tvars;
   14.18  
   14.19  
   14.20  
    15.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Dec 31 15:30:10 2008 +0100
    15.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Dec 31 18:53:16 2008 +0100
    15.3 @@ -96,7 +96,7 @@
    15.4  
    15.5      val descr' = List.concat descr;
    15.6      val recTs = get_rec_types descr' sorts;
    15.7 -    val used = foldr add_typ_tfree_names [] recTs;
    15.8 +    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
    15.9      val newTs = Library.take (length (hd descr), recTs);
   15.10  
   15.11      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
   15.12 @@ -279,7 +279,7 @@
   15.13  
   15.14      val descr' = List.concat descr;
   15.15      val recTs = get_rec_types descr' sorts;
   15.16 -    val used = foldr add_typ_tfree_names [] recTs;
   15.17 +    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
   15.18      val newTs = Library.take (length (hd descr), recTs);
   15.19      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   15.20  
    16.1 --- a/src/HOL/Tools/datatype_case.ML	Wed Dec 31 15:30:10 2008 +0100
    16.2 +++ b/src/HOL/Tools/datatype_case.ML	Wed Dec 31 18:53:16 2008 +0100
    16.3 @@ -61,8 +61,8 @@
    16.4  fun row_of_pat x = fst (snd x);
    16.5  
    16.6  fun add_row_used ((prfx, pats), (tm, tag)) used =
    16.7 -  foldl add_term_free_names (foldl add_term_free_names
    16.8 -    (add_term_free_names (tm, used)) pats) prfx;
    16.9 +  foldl OldTerm.add_term_free_names (foldl OldTerm.add_term_free_names
   16.10 +    (OldTerm.add_term_free_names (tm, used)) pats) prfx;
   16.11  
   16.12  (* try to preserve names given by user *)
   16.13  fun default_names names ts =
   16.14 @@ -139,7 +139,7 @@
   16.15                      let
   16.16                        val Ts = map type_of rstp;
   16.17                        val xs = Name.variant_list
   16.18 -                        (foldl add_term_free_names used' gvars)
   16.19 +                        (foldl OldTerm.add_term_free_names used' gvars)
   16.20                          (replicate (length rstp) "x")
   16.21                      in
   16.22                        [((prfx, gvars @ map Free (xs ~~ Ts)),
   16.23 @@ -221,7 +221,7 @@
   16.24                | SOME {case_name, constructors} =>
   16.25                  let
   16.26                    val pty = body_type cT;
   16.27 -                  val used' = foldl add_term_free_names used rstp;
   16.28 +                  val used' = foldl OldTerm.add_term_free_names used rstp;
   16.29                    val nrows = maps (expand constructors used' pty) rows;
   16.30                    val subproblems = partition ty_match ty_inst type_of used'
   16.31                      constructors pty range_ty nrows;
   16.32 @@ -335,7 +335,7 @@
   16.33          | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
   16.34        fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
   16.35              let val (l', cnstrts) = strip_constraints l
   16.36 -            in ((fst (prep_pat l' (add_term_free_names (t, []))), r), cnstrts)
   16.37 +            in ((fst (prep_pat l' (OldTerm.add_term_free_names (t, []))), r), cnstrts)
   16.38              end
   16.39          | dest_case1 t = case_error "dest_case1";
   16.40        fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   16.41 @@ -365,7 +365,7 @@
   16.42              val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
   16.43              val (xs, ys) = chop i zs;
   16.44              val u = list_abs (ys, strip_abs_body t);
   16.45 -            val xs' = map Free (Name.variant_list (add_term_names (u, used))
   16.46 +            val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
   16.47                (map fst xs) ~~ map snd xs)
   16.48            in (xs', subst_bounds (rev xs', u)) end;
   16.49          fun is_dependent i t =
   16.50 @@ -423,7 +423,7 @@
   16.51  (* destruct nested patterns *)
   16.52  
   16.53  fun strip_case' dest (pat, rhs) =
   16.54 -  case dest (add_term_free_names (pat, [])) rhs of
   16.55 +  case dest (OldTerm.add_term_free_names (pat, [])) rhs of
   16.56      SOME (exp as Free _, clauses) =>
   16.57        if member op aconv (OldTerm.term_frees pat) exp andalso
   16.58          not (exists (fn (_, rhs') =>
    17.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 15:30:10 2008 +0100
    17.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 18:53:16 2008 +0100
    17.3 @@ -216,7 +216,7 @@
    17.4        let
    17.5          val ts1 = Library.take (i, ts);
    17.6          val t :: ts2 = Library.drop (i, ts);
    17.7 -        val names = foldr add_term_names
    17.8 +        val names = foldr OldTerm.add_term_names
    17.9            (map (fst o fst o dest_Var) (foldr OldTerm.add_term_vars [] ts1)) ts1;
   17.10          val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
   17.11  
    18.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Dec 31 15:30:10 2008 +0100
    18.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 31 18:53:16 2008 +0100
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      HOL/Tools/datatype_package.ML
    18.5 -    ID:         $Id$
    18.6      Author:     Stefan Berghofer, TU Muenchen
    18.7  
    18.8  Datatype package for Isabelle/HOL.
    18.9 @@ -492,7 +491,7 @@
   18.10        ^ Syntax.string_of_typ_global thy T);
   18.11      fun type_of_constr (cT as (_, T)) =
   18.12        let
   18.13 -        val frees = typ_tfrees T;
   18.14 +        val frees = OldTerm.typ_tfrees T;
   18.15          val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
   18.16            handle TYPE _ => no_constr cT
   18.17          val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
   18.18 @@ -583,7 +582,7 @@
   18.19          fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
   18.20            let
   18.21              val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
   18.22 -            val _ = (case fold (curry add_typ_tfree_names) cargs' [] \\ tvs of
   18.23 +            val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
   18.24                  [] => ()
   18.25                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   18.26            in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
    19.1 --- a/src/HOL/Tools/datatype_prop.ML	Wed Dec 31 15:30:10 2008 +0100
    19.2 +++ b/src/HOL/Tools/datatype_prop.ML	Wed Dec 31 18:53:16 2008 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      HOL/Tools/datatype_prop.ML
    19.5 -    ID:         $Id$
    19.6      Author:     Stefan Berghofer, TU Muenchen
    19.7  
    19.8  Characteristic properties of datatypes.
    19.9 @@ -206,7 +205,7 @@
   19.10    let
   19.11      val descr' = List.concat descr;
   19.12      val recTs = get_rec_types descr' sorts;
   19.13 -    val used = foldr add_typ_tfree_names [] recTs;
   19.14 +    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
   19.15  
   19.16      val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   19.17  
   19.18 @@ -256,7 +255,7 @@
   19.19    let
   19.20      val descr' = List.concat descr;
   19.21      val recTs = get_rec_types descr' sorts;
   19.22 -    val used = foldr add_typ_tfree_names [] recTs;
   19.23 +    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
   19.24      val newTs = Library.take (length (hd descr), recTs);
   19.25      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   19.26  
   19.27 @@ -303,7 +302,7 @@
   19.28    let
   19.29      val descr' = List.concat descr;
   19.30      val recTs = get_rec_types descr' sorts;
   19.31 -    val used' = foldr add_typ_tfree_names [] recTs;
   19.32 +    val used' = foldr OldTerm.add_typ_tfree_names [] recTs;
   19.33      val newTs = Library.take (length (hd descr), recTs);
   19.34      val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   19.35      val P = Free ("P", T' --> HOLogic.boolT);
    20.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Dec 31 15:30:10 2008 +0100
    20.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Dec 31 18:53:16 2008 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      HOL/Tools/datatype_rep_proofs.ML
    20.5 -    ID:         $Id$
    20.6      Author:     Stefan Berghofer, TU Muenchen
    20.7  
    20.8  Definitional introduction of datatypes
    20.9 @@ -8,7 +7,6 @@
   20.10   - injectivity of constructors
   20.11   - distinctness of constructors
   20.12   - induction theorem
   20.13 -
   20.14  *)
   20.15  
   20.16  signature DATATYPE_REP_PROOFS =
   20.17 @@ -85,7 +83,7 @@
   20.18      val branchT = if null branchTs then HOLogic.unitT
   20.19        else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
   20.20      val arities = get_arities descr' \ 0;
   20.21 -    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
   20.22 +    val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
   20.23      val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
   20.24      val recTs = get_rec_types descr' sorts;
   20.25      val newTs = Library.take (length (hd descr), recTs);
   20.26 @@ -369,7 +367,7 @@
   20.27          val prop = Thm.prop_of thm;
   20.28          val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
   20.29            (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
   20.30 -        val used = add_term_tfree_names (a, []);
   20.31 +        val used = OldTerm.add_term_tfree_names (a, []);
   20.32  
   20.33          fun mk_thm i =
   20.34            let
    21.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 15:30:10 2008 +0100
    21.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 18:53:16 2008 +0100
    21.3 @@ -57,7 +57,7 @@
    21.4        | _ => (warn thm; thy))
    21.5      | SOME (Const (s, _), _) =>
    21.6          let
    21.7 -          val cs = foldr add_term_consts [] (prems_of thm);
    21.8 +          val cs = foldr OldTerm.add_term_consts [] (prems_of thm);
    21.9            val rules = Symtab.lookup_list intros s;
   21.10            val nparms = (case optnparms of
   21.11              SOME k => k
   21.12 @@ -490,7 +490,7 @@
   21.13        | SOME (names, thyname, nparms, intrs) =>
   21.14            mk_ind_def thy defs gr dep names (if_library thyname module)
   21.15              [] (prep_intrs intrs) nparms))
   21.16 -            (gr, foldr add_term_consts [] ts)
   21.17 +            (gr, foldr OldTerm.add_term_consts [] ts)
   21.18  
   21.19  and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   21.20    add_edge_acyclic (hd names, dep) gr handle
    22.1 --- a/src/HOL/Tools/record_package.ML	Wed Dec 31 15:30:10 2008 +0100
    22.2 +++ b/src/HOL/Tools/record_package.ML	Wed Dec 31 18:53:16 2008 +0100
    22.3 @@ -1383,14 +1383,14 @@
    22.4    let
    22.5      val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
    22.6      val T = Syntax.read_typ ctxt' raw_T;
    22.7 -    val env' = Term.add_typ_tfrees (T, env);
    22.8 +    val env' = OldTerm.add_typ_tfrees (T, env);
    22.9    in (T, env') end;
   22.10  
   22.11  fun cert_typ ctxt raw_T env =
   22.12    let
   22.13      val thy = ProofContext.theory_of ctxt;
   22.14      val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg;
   22.15 -    val env' = Term.add_typ_tfrees (T, env);
   22.16 +    val env' = OldTerm.add_typ_tfrees (T, env);
   22.17    in (T, env') end;
   22.18  
   22.19  
   22.20 @@ -1776,7 +1776,7 @@
   22.21      val names = map fst fields;
   22.22      val extN = full bname;
   22.23      val types = map snd fields;
   22.24 -    val alphas_fields = foldr add_typ_tfree_names [] types;
   22.25 +    val alphas_fields = foldr OldTerm.add_typ_tfree_names [] types;
   22.26      val alphas_ext = alphas inter alphas_fields;
   22.27      val len = length fields;
   22.28      val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
   22.29 @@ -2225,7 +2225,7 @@
   22.30      val init_env =
   22.31        (case parent of
   22.32          NONE => []
   22.33 -      | SOME (types, _) => foldr Term.add_typ_tfrees [] types);
   22.34 +      | SOME (types, _) => foldr OldTerm.add_typ_tfrees [] types);
   22.35  
   22.36  
   22.37      (* fields *)
    23.1 --- a/src/HOL/Tools/res_atp.ML	Wed Dec 31 15:30:10 2008 +0100
    23.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Dec 31 18:53:16 2008 +0100
    23.3 @@ -440,11 +440,11 @@
    23.4  fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
    23.5  
    23.6  fun tvar_classes_of_terms ts =
    23.7 -  let val sorts_list = map (map #2 o term_tvars) ts
    23.8 +  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
    23.9    in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   23.10  
   23.11  fun tfree_classes_of_terms ts =
   23.12 -  let val sorts_list = map (map #2 o term_tfrees) ts
   23.13 +  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   23.14    in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   23.15  
   23.16  (*fold type constructors*)
    24.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Dec 31 15:30:10 2008 +0100
    24.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Dec 31 18:53:16 2008 +0100
    24.3 @@ -89,7 +89,7 @@
    24.4            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
    24.5        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
    24.6            (*Universal quant: insert a free variable into body and continue*)
    24.7 -          let val fname = Name.variant (add_term_names (p, [])) a
    24.8 +          let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
    24.9            in dec_sko (subst_bound (Free (fname, T), p)) thx end
   24.10        | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   24.11        | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   24.12 @@ -117,7 +117,7 @@
   24.13              end
   24.14          | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
   24.15              (*Universal quant: insert a free variable into body and continue*)
   24.16 -            let val fname = Name.variant (add_term_names (p,[])) a
   24.17 +            let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
   24.18              in dec_sko (subst_bound (Free(fname,T), p)) defs end
   24.19          | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   24.20          | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
    25.1 --- a/src/Pure/Isar/code_unit.ML	Wed Dec 31 15:30:10 2008 +0100
    25.2 +++ b/src/Pure/Isar/code_unit.ML	Wed Dec 31 18:53:16 2008 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      Pure/Isar/code_unit.ML
    25.5 -    ID:         $Id$
    25.6      Author:     Florian Haftmann, TU Muenchen
    25.7  
    25.8  Basic notions of code generation.  Auxiliary.
    25.9 @@ -286,7 +285,7 @@
   25.10        ^ " :: " ^ string_of_typ thy ty);
   25.11      fun last_typ c_ty ty =
   25.12        let
   25.13 -        val frees = typ_tfrees ty;
   25.14 +        val frees = OldTerm.typ_tfrees ty;
   25.15          val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
   25.16            handle TYPE _ => no_constr c_ty
   25.17          val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
    26.1 --- a/src/Pure/Proof/extraction.ML	Wed Dec 31 15:30:10 2008 +0100
    26.2 +++ b/src/Pure/Proof/extraction.ML	Wed Dec 31 18:53:16 2008 +0100
    26.3 @@ -548,7 +548,7 @@
    26.4            let
    26.5              val prf = force_proof body;
    26.6              val (vs', tye) = find_inst prop Ts ts vs;
    26.7 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
    26.8 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
    26.9              val T = etype_of thy' vs' [] prop;
   26.10              val defs' = if T = nullT then defs
   26.11                else fst (extr d defs vs ts Ts hs prf0)
   26.12 @@ -569,7 +569,7 @@
   26.13                      val corr_prf' = List.foldr forall_intr_prf
   26.14                        (proof_combt
   26.15                           (PThm (serial (),
   26.16 -                          ((corr_name name vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
   26.17 +                          ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
   26.18                              Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
   26.19                        (map (get_var_type corr_prop) (vfs_of prop))
   26.20                    in
   26.21 @@ -587,7 +587,7 @@
   26.22        | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
   26.23            let
   26.24              val (vs', tye) = find_inst prop Ts ts vs;
   26.25 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   26.26 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
   26.27            in
   26.28              if etype_of thy' vs' [] prop = nullT andalso
   26.29                realizes_null vs' prop aconv prop then (defs, prf0)
   26.30 @@ -638,7 +638,7 @@
   26.31            let
   26.32              val prf = force_proof body;
   26.33              val (vs', tye) = find_inst prop Ts ts vs;
   26.34 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   26.35 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
   26.36            in
   26.37              case Symtab.lookup realizers s of
   26.38                NONE => (case find vs' (find' s defs) of
   26.39 @@ -675,12 +675,12 @@
   26.40                           (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
   26.41                             (chtype [T --> propT] reflexive_axm %> f) %%
   26.42                             PAxm (cname ^ "_def", eqn,
   26.43 -                             SOME (map TVar (term_tvars eqn))))) %% corr_prf;
   26.44 +                             SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
   26.45                      val corr_prop = Reconstruct.prop_of corr_prf';
   26.46                      val corr_prf'' = List.foldr forall_intr_prf
   26.47                        (proof_combt
   26.48                          (PThm (serial (),
   26.49 -                         ((corr_name s vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
   26.50 +                         ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
   26.51                             Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
   26.52                        (map (get_var_type corr_prop) (vfs_of prop));
   26.53                    in
   26.54 @@ -698,7 +698,7 @@
   26.55        | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
   26.56            let
   26.57              val (vs', tye) = find_inst prop Ts ts vs;
   26.58 -            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
   26.59 +            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
   26.60            in
   26.61              case find vs' (Symtab.lookup_list realizers s) of
   26.62                SOME (t, _) => (defs, subst_TVars tye' t)
    27.1 --- a/src/Pure/Proof/proofchecker.ML	Wed Dec 31 15:30:10 2008 +0100
    27.2 +++ b/src/Pure/Proof/proofchecker.ML	Wed Dec 31 18:53:16 2008 +0100
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      Pure/Proof/proofchecker.ML
    27.5 -    ID:         $Id$
    27.6      Author:     Stefan Berghofer, TU Muenchen
    27.7  
    27.8  Simple proof checker based only on the core inference rules
    27.9 @@ -37,7 +36,7 @@
   27.10  
   27.11      fun thm_of_atom thm Ts =
   27.12        let
   27.13 -        val tvars = term_tvars (Thm.full_prop_of thm);
   27.14 +        val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
   27.15          val (fmap, thm') = Thm.varifyT' [] thm;
   27.16          val ctye = map (pairself (Thm.ctyp_of thy))
   27.17            (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
    28.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Dec 31 15:30:10 2008 +0100
    28.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Dec 31 18:53:16 2008 +0100
    28.3 @@ -138,8 +138,8 @@
    28.4  
    28.5      fun mk_cnstrts_atom env vTs prop opTs prf =
    28.6            let
    28.7 -            val tvars = term_tvars prop;
    28.8 -            val tfrees = term_tfrees prop;
    28.9 +            val tvars = OldTerm.term_tvars prop;
   28.10 +            val tfrees = OldTerm.term_tfrees prop;
   28.11              val (env', Ts) = (case opTs of
   28.12                  NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
   28.13                | SOME Ts => (env, Ts));
   28.14 @@ -299,7 +299,7 @@
   28.15    end;
   28.16  
   28.17  fun prop_of_atom prop Ts = subst_atomic_types
   28.18 -  (map TVar (term_tvars prop) @ map TFree (term_tfrees prop) ~~ Ts)
   28.19 +  (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts)
   28.20    (forall_intr_vfs prop);
   28.21  
   28.22  val head_norm = Envir.head_norm (Envir.empty 0);
   28.23 @@ -366,9 +366,9 @@
   28.24                    end
   28.25                | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
   28.26                    inc (maxidx + 1) prf, prfs));
   28.27 -            val tfrees = term_tfrees prop;
   28.28 +            val tfrees = OldTerm.term_tfrees prop;
   28.29              val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
   28.30 -              (term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
   28.31 +              (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
   28.32              val varify = map_type_tfree (fn p as (a, S) =>
   28.33                if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
   28.34            in
    29.1 --- a/src/Pure/codegen.ML	Wed Dec 31 15:30:10 2008 +0100
    29.2 +++ b/src/Pure/codegen.ML	Wed Dec 31 18:53:16 2008 +0100
    29.3 @@ -277,7 +277,7 @@
    29.4  
    29.5  fun preprocess_term thy t =
    29.6    let
    29.7 -    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
    29.8 +    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
    29.9      (* fake definition *)
   29.10      val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
   29.11        (Logic.mk_equals (x, t));
   29.12 @@ -459,7 +459,7 @@
   29.13  
   29.14  fun rename_terms ts =
   29.15    let
   29.16 -    val names = List.foldr add_term_names
   29.17 +    val names = List.foldr OldTerm.add_term_names
   29.18        (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
   29.19      val reserved = filter ML_Syntax.is_reserved names;
   29.20      val (illegal, alt_names) = split_list (map_filter (fn s =>
   29.21 @@ -484,7 +484,7 @@
   29.22  (**** retrieve definition of constant ****)
   29.23  
   29.24  fun is_instance T1 T2 =
   29.25 -  Type.raw_instance (T1, if null (typ_tfrees T2) then T2 else Logic.varifyT T2);
   29.26 +  Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2);
   29.27  
   29.28  fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   29.29    s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
   29.30 @@ -598,7 +598,7 @@
   29.31  
   29.32  fun new_names t xs = Name.variant_list
   29.33    (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
   29.34 -    add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
   29.35 +    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
   29.36  
   29.37  fun new_name t x = hd (new_names t [x]);
   29.38  
    30.1 --- a/src/Pure/drule.ML	Wed Dec 31 15:30:10 2008 +0100
    30.2 +++ b/src/Pure/drule.ML	Wed Dec 31 18:53:16 2008 +0100
    30.3 @@ -367,7 +367,7 @@
    30.4           let fun newName (Var(ix,_), (pairs,used)) =
    30.5                     let val v = Name.variant used (string_of_indexname ix)
    30.6                     in  ((ix,v)::pairs, v::used)  end;
    30.7 -             val (alist, _) = List.foldr newName ([], Library.foldr add_term_names
    30.8 +             val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
    30.9                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   30.10               fun mk_inst (Var(v,T)) =
   30.11                   (cterm_of thy (Var(v,T)),
   30.12 @@ -805,8 +805,8 @@
   30.13  
   30.14  (*Increment the indexes of only the type variables*)
   30.15  fun incr_type_indexes inc th =
   30.16 -  let val tvs = term_tvars (prop_of th)
   30.17 -      and thy = theory_of_thm th
   30.18 +  let val tvs = OldTerm.term_tvars (prop_of th)
   30.19 +      and thy = Thm.theory_of_thm th
   30.20        fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
   30.21    in Thm.instantiate (map inc_tvar tvs, []) th end;
   30.22  
    31.1 --- a/src/Pure/old_term.ML	Wed Dec 31 15:30:10 2008 +0100
    31.2 +++ b/src/Pure/old_term.ML	Wed Dec 31 18:53:16 2008 +0100
    31.3 @@ -6,16 +6,89 @@
    31.4  
    31.5  signature OLD_TERM =
    31.6  sig
    31.7 +  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    31.8 +  val add_term_free_names: term * string list -> string list
    31.9 +  val add_term_names: term * string list -> string list
   31.10 +  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   31.11 +  val add_typ_tfree_names: typ * string list -> string list
   31.12 +  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   31.13 +  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   31.14 +  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   31.15 +  val add_term_tfree_names: term * string list -> string list
   31.16 +  val add_term_consts: term * string list -> string list
   31.17 +  val typ_tfrees: typ -> (string * sort) list
   31.18 +  val typ_tvars: typ -> (indexname * sort) list
   31.19 +  val term_tfrees: term -> (string * sort) list
   31.20 +  val term_tvars: term -> (indexname * sort) list
   31.21    val add_term_vars: term * term list -> term list
   31.22    val term_vars: term -> term list
   31.23    val add_term_frees: term * term list -> term list
   31.24    val term_frees: term -> term list
   31.25 +  val term_consts: term -> string list
   31.26  end;
   31.27  
   31.28  structure OldTerm: OLD_TERM =
   31.29  struct
   31.30  
   31.31 -(*Accumulates the Vars in the term, suppressing duplicates*)
   31.32 +(*iterate a function over all types in a term*)
   31.33 +fun it_term_types f =
   31.34 +let fun iter(Const(_,T), a) = f(T,a)
   31.35 +      | iter(Free(_,T), a) = f(T,a)
   31.36 +      | iter(Var(_,T), a) = f(T,a)
   31.37 +      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   31.38 +      | iter(f$u, a) = iter(f, iter(u, a))
   31.39 +      | iter(Bound _, a) = a
   31.40 +in iter end
   31.41 +
   31.42 +(*Accumulates the names of Frees in the term, suppressing duplicates.*)
   31.43 +fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
   31.44 +  | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   31.45 +  | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
   31.46 +  | add_term_free_names (_, bs) = bs;
   31.47 +
   31.48 +(*Accumulates the names in the term, suppressing duplicates.
   31.49 +  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   31.50 +fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
   31.51 +  | add_term_names (Free(a,_), bs) = insert (op =) a bs
   31.52 +  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   31.53 +  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   31.54 +  | add_term_names (_, bs) = bs;
   31.55 +
   31.56 +(*Accumulates the TVars in a type, suppressing duplicates.*)
   31.57 +fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
   31.58 +  | add_typ_tvars(TFree(_),vs) = vs
   31.59 +  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
   31.60 +
   31.61 +(*Accumulates the TFrees in a type, suppressing duplicates.*)
   31.62 +fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
   31.63 +  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
   31.64 +  | add_typ_tfree_names(TVar(_),fs) = fs;
   31.65 +
   31.66 +fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
   31.67 +  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
   31.68 +  | add_typ_tfrees(TVar(_),fs) = fs;
   31.69 +
   31.70 +(*Accumulates the TVars in a term, suppressing duplicates.*)
   31.71 +val add_term_tvars = it_term_types add_typ_tvars;
   31.72 +
   31.73 +(*Accumulates the TFrees in a term, suppressing duplicates.*)
   31.74 +val add_term_tfrees = it_term_types add_typ_tfrees;
   31.75 +val add_term_tfree_names = it_term_types add_typ_tfree_names;
   31.76 +
   31.77 +fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
   31.78 +  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   31.79 +  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   31.80 +  | add_term_consts (_, cs) = cs;
   31.81 +
   31.82 +(*Non-list versions*)
   31.83 +fun typ_tfrees T = add_typ_tfrees(T,[]);
   31.84 +fun typ_tvars T = add_typ_tvars(T,[]);
   31.85 +fun term_tfrees t = add_term_tfrees(t,[]);
   31.86 +fun term_tvars t = add_term_tvars(t,[]);
   31.87 +fun term_consts t = add_term_consts(t,[]);
   31.88 +
   31.89 +
   31.90 +(*Accumulates the Vars in the term, suppressing duplicates.*)
   31.91  fun add_term_vars (t, vars: term list) = case t of
   31.92      Var   _ => OrdList.insert TermOrd.term_ord t vars
   31.93    | Abs (_,_,body) => add_term_vars(body,vars)
   31.94 @@ -24,7 +97,7 @@
   31.95  
   31.96  fun term_vars t = add_term_vars(t,[]);
   31.97  
   31.98 -(*Accumulates the Frees in the term, suppressing duplicates*)
   31.99 +(*Accumulates the Frees in the term, suppressing duplicates.*)
  31.100  fun add_term_frees (t, frees: term list) = case t of
  31.101      Free   _ => OrdList.insert TermOrd.term_ord t frees
  31.102    | Abs (_,_,body) => add_term_frees(body,frees)
    32.1 --- a/src/Pure/proofterm.ML	Wed Dec 31 15:30:10 2008 +0100
    32.2 +++ b/src/Pure/proofterm.ML	Wed Dec 31 18:53:16 2008 +0100
    32.3 @@ -411,12 +411,12 @@
    32.4  fun del_conflicting_tvars envT T = TermSubst.instantiateT
    32.5    (map_filter (fn ixnS as (_, S) =>
    32.6       (Type.lookup envT ixnS; NONE) handle TYPE _ =>
    32.7 -        SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
    32.8 +        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
    32.9  
   32.10  fun del_conflicting_vars env t = TermSubst.instantiate
   32.11    (map_filter (fn ixnS as (_, S) =>
   32.12       (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
   32.13 -        SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
   32.14 +        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
   32.15     map_filter (fn Var (ixnT as (_, T)) =>
   32.16       (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
   32.17          SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
   32.18 @@ -612,8 +612,8 @@
   32.19  
   32.20  fun freezeT t prf =
   32.21    let
   32.22 -    val used = it_term_types add_typ_tfree_names (t, [])
   32.23 -    and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   32.24 +    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
   32.25 +    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
   32.26      val (alist, _) = List.foldr new_name ([], used) tvars;
   32.27    in
   32.28      (case alist of
    33.1 --- a/src/Pure/term.ML	Wed Dec 31 15:30:10 2008 +0100
    33.2 +++ b/src/Pure/term.ML	Wed Dec 31 18:53:16 2008 +0100
    33.3 @@ -73,8 +73,6 @@
    33.4    val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    33.5    val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    33.6    val burrow_types: (typ list -> typ list) -> term list -> term list
    33.7 -  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    33.8 -  val add_term_names: term * string list -> string list
    33.9    val aconv: term * term -> bool
   33.10    val propT: typ
   33.11    val strip_all_body: term -> term
   33.12 @@ -108,24 +106,10 @@
   33.13    val maxidx_of_typ: typ -> int
   33.14    val maxidx_of_typs: typ list -> int
   33.15    val maxidx_of_term: term -> int
   33.16 -  val add_term_consts: term * string list -> string list
   33.17 -  val term_consts: term -> string list
   33.18    val exists_subtype: (typ -> bool) -> typ -> bool
   33.19    val exists_type: (typ -> bool) -> term -> bool
   33.20    val exists_subterm: (term -> bool) -> term -> bool
   33.21    val exists_Const: (string * typ -> bool) -> term -> bool
   33.22 -  val add_term_free_names: term * string list -> string list
   33.23 -  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   33.24 -  val add_typ_tfree_names: typ * string list -> string list
   33.25 -  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   33.26 -  val add_typ_varnames: typ * string list -> string list
   33.27 -  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   33.28 -  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   33.29 -  val add_term_tfree_names: term * string list -> string list
   33.30 -  val typ_tfrees: typ -> (string * sort) list
   33.31 -  val typ_tvars: typ -> (indexname * sort) list
   33.32 -  val term_tfrees: term -> (string * sort) list
   33.33 -  val term_tvars: term -> (indexname * sort) list
   33.34    val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   33.35    val show_question_marks: bool ref
   33.36  end;
   33.37 @@ -423,29 +407,16 @@
   33.38        | map_aux (t $ u) = map_aux t $ map_aux u;
   33.39    in map_aux end;
   33.40  
   33.41 -(* iterate a function over all types in a term *)
   33.42 -fun it_term_types f =
   33.43 -let fun iter(Const(_,T), a) = f(T,a)
   33.44 -      | iter(Free(_,T), a) = f(T,a)
   33.45 -      | iter(Var(_,T), a) = f(T,a)
   33.46 -      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   33.47 -      | iter(f$u, a) = iter(f, iter(u, a))
   33.48 -      | iter(Bound _, a) = a
   33.49 -in iter end
   33.50 -
   33.51  
   33.52  (* fold types and terms *)
   33.53  
   33.54 -(*fold atoms of type*)
   33.55  fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   33.56    | fold_atyps f T = f T;
   33.57  
   33.58 -(*fold atoms of term*)
   33.59  fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   33.60    | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   33.61    | fold_aterms f a = f a;
   33.62  
   33.63 -(*fold types of term*)
   33.64  fun fold_term_types f (t as Const (_, T)) = f t T
   33.65    | fold_term_types f (t as Free (_, T)) = f t T
   33.66    | fold_term_types f (t as Var (_, T)) = f t T
   33.67 @@ -855,7 +826,7 @@
   33.68  
   33.69  
   33.70  
   33.71 -(**** Syntax-related declarations ****)
   33.72 +(** misc syntax operations **)
   33.73  
   33.74  (* substructure *)
   33.75  
   33.76 @@ -884,72 +855,13 @@
   33.77        | _ => false);
   33.78    in ex end;
   33.79  
   33.80 +fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   33.81 +
   33.82  fun has_abs (Abs _) = true
   33.83    | has_abs (t $ u) = has_abs t orelse has_abs u
   33.84    | has_abs _ = false;
   33.85  
   33.86  
   33.87 -
   33.88 -(** Consts etc. **)
   33.89 -
   33.90 -fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
   33.91 -  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   33.92 -  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   33.93 -  | add_term_consts (_, cs) = cs;
   33.94 -
   33.95 -fun term_consts t = add_term_consts(t,[]);
   33.96 -
   33.97 -fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   33.98 -
   33.99 -
  33.100 -(** TFrees and TVars **)
  33.101 -
  33.102 -(*Accumulates the names of Frees in the term, suppressing duplicates.*)
  33.103 -fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
  33.104 -  | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
  33.105 -  | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
  33.106 -  | add_term_free_names (_, bs) = bs;
  33.107 -
  33.108 -(*Accumulates the names in the term, suppressing duplicates.
  33.109 -  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
  33.110 -fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
  33.111 -  | add_term_names (Free(a,_), bs) = insert (op =) a bs
  33.112 -  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
  33.113 -  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
  33.114 -  | add_term_names (_, bs) = bs;
  33.115 -
  33.116 -(*Accumulates the TVars in a type, suppressing duplicates. *)
  33.117 -fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
  33.118 -  | add_typ_tvars(TFree(_),vs) = vs
  33.119 -  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
  33.120 -
  33.121 -(*Accumulates the TFrees in a type, suppressing duplicates. *)
  33.122 -fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
  33.123 -  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
  33.124 -  | add_typ_tfree_names(TVar(_),fs) = fs;
  33.125 -
  33.126 -fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
  33.127 -  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
  33.128 -  | add_typ_tfrees(TVar(_),fs) = fs;
  33.129 -
  33.130 -fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
  33.131 -  | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
  33.132 -  | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
  33.133 -
  33.134 -(*Accumulates the TVars in a term, suppressing duplicates. *)
  33.135 -val add_term_tvars = it_term_types add_typ_tvars;
  33.136 -
  33.137 -(*Accumulates the TFrees in a term, suppressing duplicates. *)
  33.138 -val add_term_tfrees = it_term_types add_typ_tfrees;
  33.139 -val add_term_tfree_names = it_term_types add_typ_tfree_names;
  33.140 -
  33.141 -(*Non-list versions*)
  33.142 -fun typ_tfrees T = add_typ_tfrees(T,[]);
  33.143 -fun typ_tvars T = add_typ_tvars(T,[]);
  33.144 -fun term_tfrees t = add_term_tfrees(t,[]);
  33.145 -fun term_tvars t = add_term_tvars(t,[]);
  33.146 -
  33.147 -
  33.148  (* dest abstraction *)
  33.149  
  33.150  fun dest_abs (x, T, body) =
    34.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 15:30:10 2008 +0100
    34.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 18:53:16 2008 +0100
    34.3 @@ -186,8 +186,8 @@
    34.4  (* change type-vars to fresh type frees *)
    34.5  fun fix_tvars_to_tfrees_in_terms names ts = 
    34.6      let 
    34.7 -      val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
    34.8 -      val tvars = List.foldr Term.add_term_tvars [] ts;
    34.9 +      val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
   34.10 +      val tvars = List.foldr OldTerm.add_term_tvars [] ts;
   34.11        val (names',renamings) = 
   34.12            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   34.13                           let val n2 = Name.variant Ns n in 
   34.14 @@ -212,7 +212,7 @@
   34.15  fun unfix_tfrees ns th = 
   34.16      let 
   34.17        val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
   34.18 -      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
   34.19 +      val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
   34.20      in #2 (Thm.varifyT' skiptfrees th) end;
   34.21  
   34.22  (* change schematic/meta vars to fresh free vars, avoiding name clashes 
   34.23 @@ -220,7 +220,7 @@
   34.24  fun fix_vars_to_frees_in_terms names ts = 
   34.25      let 
   34.26        val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
   34.27 -      val Ns = List.foldr Term.add_term_names names ts;
   34.28 +      val Ns = List.foldr OldTerm.add_term_names names ts;
   34.29        val (_,renamings) = 
   34.30            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   34.31                      let val n2 = Name.variant Ns n in
   34.32 @@ -245,7 +245,7 @@
   34.33        val ctypify = Thm.ctyp_of sgn
   34.34        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   34.35        val prop = (Thm.prop_of th);
   34.36 -      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
   34.37 +      val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
   34.38        val ctyfixes = 
   34.39            map_filter 
   34.40              (fn (v as ((s,i),ty)) => 
   34.41 @@ -420,7 +420,7 @@
   34.42        val t = Term.strip_all_body alledt;
   34.43        val alls = rev (Term.strip_all_vars alledt);
   34.44        val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
   34.45 -      val names = Term.add_term_names (t,varnames);
   34.46 +      val names = OldTerm.add_term_names (t,varnames);
   34.47        val fvs = map Free 
   34.48                      (Name.variant_list names (map fst alls)
   34.49                         ~~ (map snd alls));
   34.50 @@ -429,7 +429,7 @@
   34.51  fun fix_alls_term i t = 
   34.52      let 
   34.53        val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
   34.54 -      val names = Term.add_term_names (t,varnames);
   34.55 +      val names = OldTerm.add_term_names (t,varnames);
   34.56        val gt = Logic.get_goal t i;
   34.57        val body = Term.strip_all_body gt;
   34.58        val alls = rev (Term.strip_all_vars gt);
    35.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 15:30:10 2008 +0100
    35.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 18:53:16 2008 +0100
    35.3 @@ -71,7 +71,7 @@
    35.4        val (tpairl,tpairr) = Library.split_list (#tpairs rep)
    35.5        val prop = #prop rep
    35.6      in
    35.7 -      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    35.8 +      List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    35.9      end;
   35.10  
   35.11  (* Given a list of variables that were bound, and a that has been
   35.12 @@ -136,11 +136,11 @@
   35.13  fun mk_renamings tgt rule_inst = 
   35.14      let
   35.15        val rule_conds = Thm.prems_of rule_inst
   35.16 -      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
   35.17 +      val names = foldr OldTerm.add_term_names [] (tgt :: rule_conds);
   35.18        val (conds_tyvs,cond_vs) = 
   35.19            Library.foldl (fn ((tyvs, vs), t) => 
   35.20                      (Library.union
   35.21 -                       (Term.term_tvars t, tyvs),
   35.22 +                       (OldTerm.term_tvars t, tyvs),
   35.23                       Library.union 
   35.24                         (map Term.dest_Var (OldTerm.term_vars t), vs))) 
   35.25                  (([],[]), rule_conds);
   35.26 @@ -167,8 +167,8 @@
   35.27        val ignore_ixs = map fst ignore_insts;
   35.28        val (tvars, tfrees) = 
   35.29              foldr (fn (t, (varixs, tfrees)) => 
   35.30 -                      (Term.add_term_tvars (t,varixs),
   35.31 -                       Term.add_term_tfrees (t,tfrees)))
   35.32 +                      (OldTerm.add_term_tvars (t,varixs),
   35.33 +                       OldTerm.add_term_tfrees (t,tfrees)))
   35.34                    ([],[]) ts;
   35.35          val unfixed_tvars = 
   35.36              List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
    36.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Dec 31 15:30:10 2008 +0100
    36.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Dec 31 18:53:16 2008 +0100
    36.3 @@ -99,7 +99,7 @@
    36.4                 Syntax.string_of_term ctxt t);
    36.5  
    36.6    (*** Construct the fixedpoint definition ***)
    36.7 -  val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
    36.8 +  val mk_variant = Name.variant (foldr OldTerm.add_term_names [] intr_tms);
    36.9  
   36.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   36.11