# HG changeset patch
# User wenzelm
# Date 1230745996 -3600
# Node ID 0eade173f77e702be9376fbf1a81acf188c9dd21
# Parent  5c25a20129754778c16fa8d9b74ae9d2f687d0cf
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1149,7 +1149,7 @@
       val t = term_of ct
       val thy = theory_of_cterm ct
       val frees = OldTerm.term_frees t
-      val freenames = add_term_free_names (t, [])
+      val freenames = OldTerm.add_term_free_names (t, [])
       fun is_old_name n = n mem_string freenames
       fun name_of (Free (n, _)) = n
         | name_of _ = ERR "name_of"
@@ -1218,7 +1218,7 @@
                          c = "All" orelse
                          c = "op -->" orelse
                          c = "op &" orelse
-                         c = "op =")) (Term.term_consts tm)
+                         c = "op =")) (OldTerm.term_consts tm)
 
 fun match_consts t (* th *) =
     let
@@ -1423,9 +1423,9 @@
     let
         val _ = message "INST_TYPE:"
         val _ = if_debug pth hth
-        val tys_before = add_term_tfrees (prop_of th,[])
+        val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
         val th1 = Thm.varifyT th
-        val tys_after = add_term_tvars (prop_of th1,[])
+        val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
         val tyinst = map (fn (bef, iS) =>
                              (case try (Lib.assoc (TFree bef)) lambda of
                                   SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
@@ -2092,7 +2092,7 @@
             val c = case concl_of th2 of
                         _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
                       | _ => raise ERR "new_type_definition" "Bad type definition theorem"
-            val tfrees = term_tfrees c
+            val tfrees = OldTerm.term_tfrees c
             val tnames = map fst tfrees
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
@@ -2178,7 +2178,7 @@
             val c = case concl_of th2 of
                         _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
                       | _ => raise ERR "type_introduction" "Bad type definition theorem"
-            val tfrees = term_tfrees c
+            val tfrees = OldTerm.term_tfrees c
             val tnames = sort string_ord (map fst tfrees)
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -247,8 +247,8 @@
 
 fun freeze_thaw_term t =
     let
-        val tvars = term_tvars t
-        val tfree_names = add_term_tfree_names(t,[])
+        val tvars = OldTerm.term_tvars t
+        val tfree_names = OldTerm.add_term_tfree_names(t,[])
         val (type_inst,_) =
             Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
                       let
@@ -267,7 +267,7 @@
   | inst_tfrees thy ((name,U)::rest) thm =
     let
         val cU = ctyp_of thy U
-        val tfrees = add_term_tfrees (prop_of thm,[])
+        val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
         val (rens, thm') = Thm.varifyT'
     (remove (op = o apsnd fst) name tfrees) thm
         val mid =
@@ -321,7 +321,7 @@
               then
                   let
                       val cert = cterm_of thy
-                      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
+                      val v = Free(Name.variant (OldTerm.add_term_free_names(t,[])) "v",xT)
                       val cv = cert v
                       val ct = cert t
                       val th = (assume ct)
@@ -384,7 +384,7 @@
                       Type("fun",[aT,bT]) =>
                       let
                           val cert = cterm_of thy
-                          val vname = Name.variant (add_term_free_names(t,[])) "v"
+                          val vname = Name.variant (OldTerm.add_term_free_names(t,[])) "v"
                           val v = Free(vname,aT)
                           val cv = cert v
                           val ct = cert t
@@ -572,8 +572,8 @@
     fold_rev (fn thm => fn cs =>
               let
                   val (lhs,rhs) = Logic.dest_equals (prop_of thm)
-                  val ignore_lhs = term_consts lhs \\ term_consts rhs
-                  val ignore_rhs = term_consts rhs \\ term_consts lhs
+                  val ignore_lhs = OldTerm.term_consts lhs \\ OldTerm.term_consts rhs
+                  val ignore_rhs = OldTerm.term_consts rhs \\ OldTerm.term_consts lhs
               in
                   fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
               end)
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Inductive.thy	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Inductive.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
@@ -363,7 +362,7 @@
 let
   fun fun_tr ctxt [cs] =
     let
-      val x = Free (Name.variant (add_term_free_names (cs, [])) "x", dummyT);
+      val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
       val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
                  ctxt [x, cs]
     in lambda x ft end
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Efficient_Nat.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
 *)
 
@@ -170,7 +169,7 @@
 fun eqn_suc_preproc thy ths =
   let
     val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
-    fun contains_suc t = member (op =) (term_consts t) @{const_name Suc};
+    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
   in
     if forall (can dest) ths andalso
       exists (contains_suc o dest) ths
@@ -212,7 +211,7 @@
     val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   in
     if forall (can (dest o concl_of)) ths andalso
-      exists (fn th => member (op =) (foldr add_term_consts
+      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
         [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
     then remove_suc_clause thy ths else ths
   end;
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/List.thy	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/List.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
 *)
 
@@ -359,7 +358,7 @@
 
    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     let
-      val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT);
+      val x = Free (Name.variant (OldTerm.add_term_free_names (p$e, [])) "x", dummyT);
       val e = if opti then singl e else e;
       val case1 = Syntax.const "_case1" $ p $ e;
       val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Matrix/cplex/matrixlp.ML
--- a/src/HOL/Matrix/cplex/matrixlp.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Matrix/cplex/matrixlp.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Matrix/cplex/matrixlp.ML
-    ID:         $Id$
     Author:     Steven Obua
 *)
 
@@ -20,7 +19,7 @@
 fun inst_real thm =
   let val certT = ctyp_of (Thm.theory_of_thm thm) in
     standard (Thm.instantiate
-      ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
+      ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
   end
 
 local
@@ -58,7 +57,7 @@
     let
         val certT = Thm.ctyp_of (Thm.theory_of_thm thm);
         val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
-        val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
+        val v = TVar (hd (sort ord (OldTerm.term_tvars (prop_of thm))))
     in
         standard (Thm.instantiate ([(certT v, certT ty)], []) thm)
     end
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -247,7 +247,7 @@
 (* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw
    and thm.instantiate *)
 fun freeze_thaw t =
-  let val used = add_term_names (t, [])
+  let val used = OldTerm.add_term_names (t, [])
           and vars = OldTerm.term_vars t;
       fun newName (Var(ix,_), (pairs,used)) = 
           let val v = Name.variant used (string_of_indexname ix)
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -152,7 +152,7 @@
     val elims = map (atomize_induct ctxt) elims;
     val monos = InductivePackage.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
-    val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
+    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
@@ -199,8 +199,8 @@
     val ind_sort = if null atomTs then HOLogic.typeS
       else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
         ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs);
-    val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n";
-    val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z";
+    val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
+    val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
 
     val inductive_forall_def' = Drule.instantiate'
@@ -411,7 +411,7 @@
       let
         val prem :: prems = Logic.strip_imp_prems rule;
         val concl = Logic.strip_imp_concl rule;
-        val used = add_term_free_names (rule, [])
+        val used = OldTerm.add_term_free_names (rule, [])
       in
         (prem,
          List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params),
@@ -613,7 +613,7 @@
       [mk_perm_bool_simproc names,
        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val t = Logic.unvarify (concl_of raw_induct);
-    val pi = Name.variant (add_term_names (t, [])) "pi";
+    val pi = Name.variant (OldTerm.add_term_names (t, [])) "pi";
     val ps = map (fst o HOLogic.dest_imp)
       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
     fun eqvt_tac pi (intr, vs) st =
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -158,7 +158,7 @@
     val elims = map (atomize_induct ctxt) elims;
     val monos = InductivePackage.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
-    val _ = (case names \\ foldl (apfst prop_of #> add_term_consts) [] eqvt_thms of
+    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
@@ -221,8 +221,8 @@
     val ind_sort = if null atomTs then HOLogic.typeS
       else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
         ("fs_" ^ Sign.base_name a)) atoms);
-    val fs_ctxt_tyname = Name.variant (map fst (term_tfrees raw_induct')) "'n";
-    val fs_ctxt_name = Name.variant (add_term_names (raw_induct', [])) "z";
+    val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
+    val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
 
     val inductive_forall_def' = Drule.instantiate'
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Nominal/nominal_package.ML
-    ID:         $Id$
     Author:     Stefan Berghofer and Christian Urban, TU Muenchen
 
 Nominal datatype package for Isabelle/HOL.
@@ -1414,7 +1413,7 @@
 
     val _ = warning "defining recursion combinator ...";
 
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
 
     val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used;
 
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -123,7 +123,7 @@
 
       val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
 
-      val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
+      val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
       val (Pv, Dv, type_insts) =
           case (Thm.concl_of case_thm) of
             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -514,7 +514,7 @@
                 val (f,args) = S.strip_comb (get_lhs eq)
                 val (vstrl,_) = S.strip_abs f
                 val names  =
-                  Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
+                  Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
             in get (rst, n+1, (names,n)::L) end
             handle TERM _ => get (rst, n+1, L)
               | U.ERR _ => get (rst, n+1, L);
@@ -803,7 +803,7 @@
     (if (is_cong thm) then cong_prover else restrict_prover) ss thm
     end
     val ctm = cprop_of th
-    val names = add_term_names (term_of ctm, [])
+    val names = OldTerm.add_term_names (term_of ctm, [])
     val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
       (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
     val th2 = equal_elim th1 th
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Tools/TFL/tfl.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 
 First part of main module.
 *)
@@ -332,7 +330,7 @@
      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
                               map (fn (t,i) => (t,(i,true))) (enumerate R))
-     val names = foldr add_term_names [] R
+     val names = foldr OldTerm.add_term_names [] R
      val atype = type_of(hd pats)
      and aname = Name.variant names "a"
      val a = Free(aname,atype)
@@ -494,7 +492,7 @@
      val tych = Thry.typecheck thy
      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
      val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
-     val R = Free (Name.variant (foldr add_term_names [] eqns) Rname,
+     val R = Free (Name.variant (foldr OldTerm.add_term_names [] eqns) Rname,
                    Rtype)
      val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
      val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
@@ -692,7 +690,7 @@
  let val tych = Thry.typecheck thy
      val ty_info = Thry.induct_info thy
  in fn pats =>
- let val names = foldr add_term_names [] pats
+ let val names = foldr OldTerm.add_term_names [] pats
      val T = type_of (hd pats)
      val aname = Name.variant names "a"
      val vname = Name.variant (aname::names) "v"
@@ -845,7 +843,7 @@
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
     val domain = (type_of o hd) pats
-    val Pname = Name.variant (foldr (Library.foldr add_term_names)
+    val Pname = Name.variant (foldr (Library.foldr OldTerm.add_term_names)
                               [] (pats::TCsl)) "P"
     val P = Free(Pname, domain --> HOLogic.boolT)
     val Sinduct = R.SPEC (tych P) Sinduction
@@ -856,7 +854,7 @@
     val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
     val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
     val proved_cases = map (prove_case fconst thy) tasks
-    val v = Free (Name.variant (foldr add_term_names [] (map concl proved_cases))
+    val v = Free (Name.variant (foldr OldTerm.add_term_names [] (map concl proved_cases))
                     "v",
                   domain)
     val vtyped = tych v
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -112,7 +112,7 @@
 
 val is_vartype = can dest_vtype;
 
-val type_vars  = map mk_prim_vartype o typ_tvars
+val type_vars  = map mk_prim_vartype o OldTerm.typ_tvars
 fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
 
 val alpha  = mk_vartype "'a"
@@ -142,7 +142,7 @@
 
 
 
-val type_vars_in_term = map mk_prim_vartype o term_tvars;
+val type_vars_in_term = map mk_prim_vartype o OldTerm.term_tvars;
 
 
 
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -96,7 +96,7 @@
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
 
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
@@ -279,7 +279,7 @@
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/datatype_case.ML
--- a/src/HOL/Tools/datatype_case.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_case.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -61,8 +61,8 @@
 fun row_of_pat x = fst (snd x);
 
 fun add_row_used ((prfx, pats), (tm, tag)) used =
-  foldl add_term_free_names (foldl add_term_free_names
-    (add_term_free_names (tm, used)) pats) prfx;
+  foldl OldTerm.add_term_free_names (foldl OldTerm.add_term_free_names
+    (OldTerm.add_term_free_names (tm, used)) pats) prfx;
 
 (* try to preserve names given by user *)
 fun default_names names ts =
@@ -139,7 +139,7 @@
                     let
                       val Ts = map type_of rstp;
                       val xs = Name.variant_list
-                        (foldl add_term_free_names used' gvars)
+                        (foldl OldTerm.add_term_free_names used' gvars)
                         (replicate (length rstp) "x")
                     in
                       [((prfx, gvars @ map Free (xs ~~ Ts)),
@@ -221,7 +221,7 @@
               | SOME {case_name, constructors} =>
                 let
                   val pty = body_type cT;
-                  val used' = foldl add_term_free_names used rstp;
+                  val used' = foldl OldTerm.add_term_free_names used rstp;
                   val nrows = maps (expand constructors used' pty) rows;
                   val subproblems = partition ty_match ty_inst type_of used'
                     constructors pty range_ty nrows;
@@ -335,7 +335,7 @@
         | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
       fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
             let val (l', cnstrts) = strip_constraints l
-            in ((fst (prep_pat l' (add_term_free_names (t, []))), r), cnstrts)
+            in ((fst (prep_pat l' (OldTerm.add_term_free_names (t, []))), r), cnstrts)
             end
         | dest_case1 t = case_error "dest_case1";
       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
@@ -365,7 +365,7 @@
             val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
             val (xs, ys) = chop i zs;
             val u = list_abs (ys, strip_abs_body t);
-            val xs' = map Free (Name.variant_list (add_term_names (u, used))
+            val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
               (map fst xs) ~~ map snd xs)
           in (xs', subst_bounds (rev xs', u)) end;
         fun is_dependent i t =
@@ -423,7 +423,7 @@
 (* destruct nested patterns *)
 
 fun strip_case' dest (pat, rhs) =
-  case dest (add_term_free_names (pat, [])) rhs of
+  case dest (OldTerm.add_term_free_names (pat, [])) rhs of
     SOME (exp as Free _, clauses) =>
       if member op aconv (OldTerm.term_frees pat) exp andalso
         not (exists (fn (_, rhs') =>
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -216,7 +216,7 @@
       let
         val ts1 = Library.take (i, ts);
         val t :: ts2 = Library.drop (i, ts);
-        val names = foldr add_term_names
+        val names = foldr OldTerm.add_term_names
           (map (fst o fst o dest_Var) (foldr OldTerm.add_term_vars [] ts1)) ts1;
         val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
 
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/datatype_package.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Datatype package for Isabelle/HOL.
@@ -492,7 +491,7 @@
       ^ Syntax.string_of_typ_global thy T);
     fun type_of_constr (cT as (_, T)) =
       let
-        val frees = typ_tfrees T;
+        val frees = OldTerm.typ_tfrees T;
         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
           handle TYPE _ => no_constr cT
         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
@@ -583,7 +582,7 @@
         fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
           let
             val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
-            val _ = (case fold (curry add_typ_tfree_names) cargs' [] \\ tvs of
+            val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
           in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/datatype_prop.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Characteristic properties of datatypes.
@@ -206,7 +205,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
 
     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
 
@@ -256,7 +255,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names [] recTs;
+    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
@@ -303,7 +302,7 @@
   let
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
-    val used' = foldr add_typ_tfree_names [] recTs;
+    val used' = foldr OldTerm.add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
     val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/datatype_rep_proofs.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Definitional introduction of datatypes
@@ -8,7 +7,6 @@
  - injectivity of constructors
  - distinctness of constructors
  - induction theorem
-
 *)
 
 signature DATATYPE_REP_PROOFS =
@@ -85,7 +83,7 @@
     val branchT = if null branchTs then HOLogic.unitT
       else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     val arities = get_arities descr' \ 0;
-    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
+    val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
     val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
@@ -369,7 +367,7 @@
         val prop = Thm.prop_of thm;
         val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
-        val used = add_term_tfree_names (a, []);
+        val used = OldTerm.add_term_tfree_names (a, []);
 
         fun mk_thm i =
           let
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -57,7 +57,7 @@
       | _ => (warn thm; thy))
     | SOME (Const (s, _), _) =>
         let
-          val cs = foldr add_term_consts [] (prems_of thm);
+          val cs = foldr OldTerm.add_term_consts [] (prems_of thm);
           val rules = Symtab.lookup_list intros s;
           val nparms = (case optnparms of
             SOME k => k
@@ -490,7 +490,7 @@
       | SOME (names, thyname, nparms, intrs) =>
           mk_ind_def thy defs gr dep names (if_library thyname module)
             [] (prep_intrs intrs) nparms))
-            (gr, foldr add_term_consts [] ts)
+            (gr, foldr OldTerm.add_term_consts [] ts)
 
 and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   add_edge_acyclic (hd names, dep) gr handle
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1383,14 +1383,14 @@
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     val T = Syntax.read_typ ctxt' raw_T;
-    val env' = Term.add_typ_tfrees (T, env);
+    val env' = OldTerm.add_typ_tfrees (T, env);
   in (T, env') end;
 
 fun cert_typ ctxt raw_T env =
   let
     val thy = ProofContext.theory_of ctxt;
     val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg;
-    val env' = Term.add_typ_tfrees (T, env);
+    val env' = OldTerm.add_typ_tfrees (T, env);
   in (T, env') end;
 
 
@@ -1776,7 +1776,7 @@
     val names = map fst fields;
     val extN = full bname;
     val types = map snd fields;
-    val alphas_fields = foldr add_typ_tfree_names [] types;
+    val alphas_fields = foldr OldTerm.add_typ_tfree_names [] types;
     val alphas_ext = alphas inter alphas_fields;
     val len = length fields;
     val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
@@ -2225,7 +2225,7 @@
     val init_env =
       (case parent of
         NONE => []
-      | SOME (types, _) => foldr Term.add_typ_tfrees [] types);
+      | SOME (types, _) => foldr OldTerm.add_typ_tfrees [] types);
 
 
     (* fields *)
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -440,11 +440,11 @@
 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
 
 fun tvar_classes_of_terms ts =
-  let val sorts_list = map (map #2 o term_tvars) ts
+  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
 
 fun tfree_classes_of_terms ts =
-  let val sorts_list = map (map #2 o term_tfrees) ts
+  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
 
 (*fold type constructors*)
diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -89,7 +89,7 @@
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
       | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
           (*Universal quant: insert a free variable into body and continue*)
-          let val fname = Name.variant (add_term_names (p, [])) a
+          let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
           in dec_sko (subst_bound (Free (fname, T), p)) thx end
       | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
       | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
@@ -117,7 +117,7 @@
             end
         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
             (*Universal quant: insert a free variable into body and continue*)
-            let val fname = Name.variant (add_term_names (p,[])) a
+            let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
             in dec_sko (subst_bound (Free(fname,T), p)) defs end
         | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
         | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/Isar/code_unit.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/code_unit.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Basic notions of code generation.  Auxiliary.
@@ -286,7 +285,7 @@
       ^ " :: " ^ string_of_typ thy ty);
     fun last_typ c_ty ty =
       let
-        val frees = typ_tfrees ty;
+        val frees = OldTerm.typ_tfrees ty;
         val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
           handle TYPE _ => no_constr c_ty
         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -548,7 +548,7 @@
           let
             val prf = force_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
+            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
             val T = etype_of thy' vs' [] prop;
             val defs' = if T = nullT then defs
               else fst (extr d defs vs ts Ts hs prf0)
@@ -569,7 +569,7 @@
                     val corr_prf' = List.foldr forall_intr_prf
                       (proof_combt
                          (PThm (serial (),
-                          ((corr_name name vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
+                          ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
                             Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop))
                   in
@@ -587,7 +587,7 @@
       | corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
+            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
           in
             if etype_of thy' vs' [] prop = nullT andalso
               realizes_null vs' prop aconv prop then (defs, prf0)
@@ -638,7 +638,7 @@
           let
             val prf = force_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
+            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
           in
             case Symtab.lookup realizers s of
               NONE => (case find vs' (find' s defs) of
@@ -675,12 +675,12 @@
                          (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
                            (chtype [T --> propT] reflexive_axm %> f) %%
                            PAxm (cname ^ "_def", eqn,
-                             SOME (map TVar (term_tvars eqn))))) %% corr_prf;
+                             SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
                     val corr_prop = Reconstruct.prop_of corr_prf';
                     val corr_prf'' = List.foldr forall_intr_prf
                       (proof_combt
                         (PThm (serial (),
-                         ((corr_name s vs', corr_prop, SOME (map TVar (term_tvars corr_prop))),
+                         ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
                            Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop));
                   in
@@ -698,7 +698,7 @@
       | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
-            val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
+            val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
           in
             case find vs' (Symtab.lookup_list realizers s) of
               SOME (t, _) => (defs, subst_TVars tye' t)
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Proof/proofchecker.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Simple proof checker based only on the core inference rules
@@ -37,7 +36,7 @@
 
     fun thm_of_atom thm Ts =
       let
-        val tvars = term_tvars (Thm.full_prop_of thm);
+        val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
         val (fmap, thm') = Thm.varifyT' [] thm;
         val ctye = map (pairself (Thm.ctyp_of thy))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -138,8 +138,8 @@
 
     fun mk_cnstrts_atom env vTs prop opTs prf =
           let
-            val tvars = term_tvars prop;
-            val tfrees = term_tfrees prop;
+            val tvars = OldTerm.term_tvars prop;
+            val tfrees = OldTerm.term_tfrees prop;
             val (env', Ts) = (case opTs of
                 NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
               | SOME Ts => (env, Ts));
@@ -299,7 +299,7 @@
   end;
 
 fun prop_of_atom prop Ts = subst_atomic_types
-  (map TVar (term_tvars prop) @ map TFree (term_tfrees prop) ~~ Ts)
+  (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts)
   (forall_intr_vfs prop);
 
 val head_norm = Envir.head_norm (Envir.empty 0);
@@ -366,9 +366,9 @@
                   end
               | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
                   inc (maxidx + 1) prf, prfs));
-            val tfrees = term_tfrees prop;
+            val tfrees = OldTerm.term_tfrees prop;
             val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
-              (term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
+              (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
             val varify = map_type_tfree (fn p as (a, S) =>
               if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
           in
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/codegen.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -277,7 +277,7 @@
 
 fun preprocess_term thy t =
   let
-    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
+    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
     (* fake definition *)
     val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
       (Logic.mk_equals (x, t));
@@ -459,7 +459,7 @@
 
 fun rename_terms ts =
   let
-    val names = List.foldr add_term_names
+    val names = List.foldr OldTerm.add_term_names
       (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
     val reserved = filter ML_Syntax.is_reserved names;
     val (illegal, alt_names) = split_list (map_filter (fn s =>
@@ -484,7 +484,7 @@
 (**** retrieve definition of constant ****)
 
 fun is_instance T1 T2 =
-  Type.raw_instance (T1, if null (typ_tfrees T2) then T2 else Logic.varifyT T2);
+  Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2);
 
 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
@@ -598,7 +598,7 @@
 
 fun new_names t xs = Name.variant_list
   (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
-    add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
+    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
 
 fun new_name t x = hd (new_names t [x]);
 
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/drule.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -367,7 +367,7 @@
          let fun newName (Var(ix,_), (pairs,used)) =
                    let val v = Name.variant used (string_of_indexname ix)
                    in  ((ix,v)::pairs, v::used)  end;
-             val (alist, _) = List.foldr newName ([], Library.foldr add_term_names
+             val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
                (prop :: Thm.terms_of_tpairs tpairs, [])) vars
              fun mk_inst (Var(v,T)) =
                  (cterm_of thy (Var(v,T)),
@@ -805,8 +805,8 @@
 
 (*Increment the indexes of only the type variables*)
 fun incr_type_indexes inc th =
-  let val tvs = term_tvars (prop_of th)
-      and thy = theory_of_thm th
+  let val tvs = OldTerm.term_tvars (prop_of th)
+      and thy = Thm.theory_of_thm th
       fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
   in Thm.instantiate (map inc_tvar tvs, []) th end;
 
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/old_term.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -6,16 +6,89 @@
 
 signature OLD_TERM =
 sig
+  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
+  val add_term_free_names: term * string list -> string list
+  val add_term_names: term * string list -> string list
+  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
+  val add_typ_tfree_names: typ * string list -> string list
+  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
+  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
+  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
+  val add_term_tfree_names: term * string list -> string list
+  val add_term_consts: term * string list -> string list
+  val typ_tfrees: typ -> (string * sort) list
+  val typ_tvars: typ -> (indexname * sort) list
+  val term_tfrees: term -> (string * sort) list
+  val term_tvars: term -> (indexname * sort) list
   val add_term_vars: term * term list -> term list
   val term_vars: term -> term list
   val add_term_frees: term * term list -> term list
   val term_frees: term -> term list
+  val term_consts: term -> string list
 end;
 
 structure OldTerm: OLD_TERM =
 struct
 
-(*Accumulates the Vars in the term, suppressing duplicates*)
+(*iterate a function over all types in a term*)
+fun it_term_types f =
+let fun iter(Const(_,T), a) = f(T,a)
+      | iter(Free(_,T), a) = f(T,a)
+      | iter(Var(_,T), a) = f(T,a)
+      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
+      | iter(f$u, a) = iter(f, iter(u, a))
+      | iter(Bound _, a) = a
+in iter end
+
+(*Accumulates the names of Frees in the term, suppressing duplicates.*)
+fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
+  | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
+  | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
+  | add_term_free_names (_, bs) = bs;
+
+(*Accumulates the names in the term, suppressing duplicates.
+  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
+fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
+  | add_term_names (Free(a,_), bs) = insert (op =) a bs
+  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
+  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
+  | add_term_names (_, bs) = bs;
+
+(*Accumulates the TVars in a type, suppressing duplicates.*)
+fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
+  | add_typ_tvars(TFree(_),vs) = vs
+  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
+
+(*Accumulates the TFrees in a type, suppressing duplicates.*)
+fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
+  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
+  | add_typ_tfree_names(TVar(_),fs) = fs;
+
+fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
+  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
+  | add_typ_tfrees(TVar(_),fs) = fs;
+
+(*Accumulates the TVars in a term, suppressing duplicates.*)
+val add_term_tvars = it_term_types add_typ_tvars;
+
+(*Accumulates the TFrees in a term, suppressing duplicates.*)
+val add_term_tfrees = it_term_types add_typ_tfrees;
+val add_term_tfree_names = it_term_types add_typ_tfree_names;
+
+fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
+  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
+  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
+  | add_term_consts (_, cs) = cs;
+
+(*Non-list versions*)
+fun typ_tfrees T = add_typ_tfrees(T,[]);
+fun typ_tvars T = add_typ_tvars(T,[]);
+fun term_tfrees t = add_term_tfrees(t,[]);
+fun term_tvars t = add_term_tvars(t,[]);
+fun term_consts t = add_term_consts(t,[]);
+
+
+(*Accumulates the Vars in the term, suppressing duplicates.*)
 fun add_term_vars (t, vars: term list) = case t of
     Var   _ => OrdList.insert TermOrd.term_ord t vars
   | Abs (_,_,body) => add_term_vars(body,vars)
@@ -24,7 +97,7 @@
 
 fun term_vars t = add_term_vars(t,[]);
 
-(*Accumulates the Frees in the term, suppressing duplicates*)
+(*Accumulates the Frees in the term, suppressing duplicates.*)
 fun add_term_frees (t, frees: term list) = case t of
     Free   _ => OrdList.insert TermOrd.term_ord t frees
   | Abs (_,_,body) => add_term_frees(body,frees)
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/proofterm.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -411,12 +411,12 @@
 fun del_conflicting_tvars envT T = TermSubst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup envT ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
+        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
 
 fun del_conflicting_vars env t = TermSubst.instantiate
   (map_filter (fn ixnS as (_, S) =>
      (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
+        SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
    map_filter (fn Var (ixnT as (_, T)) =>
      (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
         SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
@@ -612,8 +612,8 @@
 
 fun freezeT t prf =
   let
-    val used = it_term_types add_typ_tfree_names (t, [])
-    and tvars = map #1 (it_term_types add_typ_tvars (t, []));
+    val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
+    and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
     val (alist, _) = List.foldr new_name ([], used) tvars;
   in
     (case alist of
diff -r 5c25a2012975 -r 0eade173f77e src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/term.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -73,8 +73,6 @@
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
   val burrow_types: (typ list -> typ list) -> term list -> term list
-  val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
-  val add_term_names: term * string list -> string list
   val aconv: term * term -> bool
   val propT: typ
   val strip_all_body: term -> term
@@ -108,24 +106,10 @@
   val maxidx_of_typ: typ -> int
   val maxidx_of_typs: typ list -> int
   val maxidx_of_term: term -> int
-  val add_term_consts: term * string list -> string list
-  val term_consts: term -> string list
   val exists_subtype: (typ -> bool) -> typ -> bool
   val exists_type: (typ -> bool) -> term -> bool
   val exists_subterm: (term -> bool) -> term -> bool
   val exists_Const: (string * typ -> bool) -> term -> bool
-  val add_term_free_names: term * string list -> string list
-  val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
-  val add_typ_tfree_names: typ * string list -> string list
-  val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
-  val add_typ_varnames: typ * string list -> string list
-  val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
-  val add_term_tfrees: term * (string * sort) list -> (string * sort) list
-  val add_term_tfree_names: term * string list -> string list
-  val typ_tfrees: typ -> (string * sort) list
-  val typ_tvars: typ -> (indexname * sort) list
-  val term_tfrees: term -> (string * sort) list
-  val term_tvars: term -> (indexname * sort) list
   val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   val show_question_marks: bool ref
 end;
@@ -423,29 +407,16 @@
       | map_aux (t $ u) = map_aux t $ map_aux u;
   in map_aux end;
 
-(* iterate a function over all types in a term *)
-fun it_term_types f =
-let fun iter(Const(_,T), a) = f(T,a)
-      | iter(Free(_,T), a) = f(T,a)
-      | iter(Var(_,T), a) = f(T,a)
-      | iter(Abs(_,T,t), a) = iter(t,f(T,a))
-      | iter(f$u, a) = iter(f, iter(u, a))
-      | iter(Bound _, a) = a
-in iter end
-
 
 (* fold types and terms *)
 
-(*fold atoms of type*)
 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   | fold_atyps f T = f T;
 
-(*fold atoms of term*)
 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   | fold_aterms f a = f a;
 
-(*fold types of term*)
 fun fold_term_types f (t as Const (_, T)) = f t T
   | fold_term_types f (t as Free (_, T)) = f t T
   | fold_term_types f (t as Var (_, T)) = f t T
@@ -855,7 +826,7 @@
 
 
 
-(**** Syntax-related declarations ****)
+(** misc syntax operations **)
 
 (* substructure *)
 
@@ -884,72 +855,13 @@
       | _ => false);
   in ex end;
 
+fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
+
 fun has_abs (Abs _) = true
   | has_abs (t $ u) = has_abs t orelse has_abs u
   | has_abs _ = false;
 
 
-
-(** Consts etc. **)
-
-fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
-  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
-  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
-  | add_term_consts (_, cs) = cs;
-
-fun term_consts t = add_term_consts(t,[]);
-
-fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
-
-
-(** TFrees and TVars **)
-
-(*Accumulates the names of Frees in the term, suppressing duplicates.*)
-fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
-  | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
-  | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
-  | add_term_free_names (_, bs) = bs;
-
-(*Accumulates the names in the term, suppressing duplicates.
-  Includes Frees and Consts.  For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
-  | add_term_names (Free(a,_), bs) = insert (op =) a bs
-  | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
-  | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
-  | add_term_names (_, bs) = bs;
-
-(*Accumulates the TVars in a type, suppressing duplicates. *)
-fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
-  | add_typ_tvars(TFree(_),vs) = vs
-  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
-
-(*Accumulates the TFrees in a type, suppressing duplicates. *)
-fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
-  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
-  | add_typ_tfree_names(TVar(_),fs) = fs;
-
-fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
-  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
-  | add_typ_tfrees(TVar(_),fs) = fs;
-
-fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
-  | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
-  | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
-
-(*Accumulates the TVars in a term, suppressing duplicates. *)
-val add_term_tvars = it_term_types add_typ_tvars;
-
-(*Accumulates the TFrees in a term, suppressing duplicates. *)
-val add_term_tfrees = it_term_types add_typ_tfrees;
-val add_term_tfree_names = it_term_types add_typ_tfree_names;
-
-(*Non-list versions*)
-fun typ_tfrees T = add_typ_tfrees(T,[]);
-fun typ_tvars T = add_typ_tvars(T,[]);
-fun term_tfrees t = add_term_tfrees(t,[]);
-fun term_tvars t = add_term_tvars(t,[]);
-
-
 (* dest abstraction *)
 
 fun dest_abs (x, T, body) =
diff -r 5c25a2012975 -r 0eade173f77e src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -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 Term.add_term_tfrees [] ts);
-      val tvars = List.foldr Term.add_term_tvars [] ts;
+      val tfree_names = map fst (List.foldr OldTerm.add_term_tfrees [] ts);
+      val tvars = List.foldr OldTerm.add_term_tvars [] ts;
       val (names',renamings) = 
           List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
                          let val n2 = Name.variant Ns n in 
@@ -212,7 +212,7 @@
 fun unfix_tfrees ns th = 
     let 
       val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
-      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
+      val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
     in #2 (Thm.varifyT' skiptfrees th) end;
 
 (* change schematic/meta vars to fresh free vars, avoiding name clashes 
@@ -220,7 +220,7 @@
 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 Term.add_term_names names ts;
+      val Ns = List.foldr OldTerm.add_term_names names ts;
       val (_,renamings) = 
           Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
                     let val n2 = Name.variant 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 Term.add_term_tvars [] (prop :: tpairs);
+      val tvars = List.foldr OldTerm.add_term_tvars [] (prop :: tpairs);
       val ctyfixes = 
           map_filter 
             (fn (v as ((s,i),ty)) => 
@@ -420,7 +420,7 @@
       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 = Term.add_term_names (t,varnames);
+      val names = OldTerm.add_term_names (t,varnames);
       val fvs = map Free 
                     (Name.variant_list names (map fst alls)
                        ~~ (map snd alls));
@@ -429,7 +429,7 @@
 fun fix_alls_term i t = 
     let 
       val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
-      val names = Term.add_term_names (t,varnames);
+      val names = OldTerm.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);
diff -r 5c25a2012975 -r 0eade173f77e src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -71,7 +71,7 @@
       val (tpairl,tpairr) = Library.split_list (#tpairs rep)
       val prop = #prop rep
     in
-      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
+      List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
     end;
 
 (* Given a list of variables that were bound, and a that has been
@@ -136,11 +136,11 @@
 fun mk_renamings tgt rule_inst = 
     let
       val rule_conds = Thm.prems_of rule_inst
-      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
+      val names = foldr OldTerm.add_term_names [] (tgt :: rule_conds);
       val (conds_tyvs,cond_vs) = 
           Library.foldl (fn ((tyvs, vs), t) => 
                     (Library.union
-                       (Term.term_tvars t, tyvs),
+                       (OldTerm.term_tvars t, tyvs),
                      Library.union 
                        (map Term.dest_Var (OldTerm.term_vars t), vs))) 
                 (([],[]), rule_conds);
@@ -167,8 +167,8 @@
       val ignore_ixs = map fst ignore_insts;
       val (tvars, tfrees) = 
             foldr (fn (t, (varixs, tfrees)) => 
-                      (Term.add_term_tvars (t,varixs),
-                       Term.add_term_tfrees (t,tfrees)))
+                      (OldTerm.add_term_tvars (t,varixs),
+                       OldTerm.add_term_tfrees (t,tfrees)))
                   ([],[]) ts;
         val unfixed_tvars = 
             List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
diff -r 5c25a2012975 -r 0eade173f77e src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -99,7 +99,7 @@
                Syntax.string_of_term ctxt t);
 
   (*** Construct the fixedpoint definition ***)
-  val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
+  val mk_variant = Name.variant (foldr OldTerm.add_term_names [] intr_tms);
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";