# HG changeset patch
# User wenzelm
# Date 1230678493 -3600
# Node ID 5b4247055bd7132db922dcf4c75a2b1ab839556d
# Parent  4ea3358fac3fa3691562973984f5bd8f6cac1c91
moved old add_term_vars, add_term_frees etc. to structure OldTerm;

diff -r 4ea3358fac3f -r 5b4247055bd7 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/FOLP/simp.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
-(*  Title:      FOLP/simp
-    ID:         $Id$
+(*  Title:      FOLP/simp.ML
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
 
@@ -156,21 +155,21 @@
 (*ccs contains the names of the constants possessing congruence rules*)
 fun add_hidden_vars ccs =
   let fun add_hvars tm hvars = case tm of
-              Abs(_,_,body) => add_term_vars(body,hvars)
+              Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
             | _$_ => let val (f,args) = strip_comb tm 
                      in case f of
                             Const(c,T) => 
                                 if member (op =) ccs c
                                 then fold_rev add_hvars args hvars
-                                else add_term_vars (tm, hvars)
-                          | _ => add_term_vars (tm, hvars)
+                                else OldTerm.add_term_vars (tm, hvars)
+                          | _ => OldTerm.add_term_vars (tm, hvars)
                      end
             | _ => hvars;
   in add_hvars end;
 
 fun add_new_asm_vars new_asms =
     let fun itf (tm, at) vars =
-                if at then vars else add_term_vars(tm,vars)
+                if at then vars else OldTerm.add_term_vars(tm,vars)
         fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
                 in if length(tml)=length(al)
                    then fold_rev itf (tml ~~ al) vars
@@ -198,7 +197,7 @@
     val hvars = add_new_asm_vars new_asms (rhs,hvars)
     fun it_asms asm hvars =
         if atomic asm then add_new_asm_vars new_asms (asm,hvars)
-        else add_term_frees(asm,hvars)
+        else OldTerm.add_term_frees(asm,hvars)
     val hvars = fold_rev it_asms asms hvars
     val hvs = map (#1 o dest_Var) hvars
     val refl1_tac = refl_tac 1
@@ -542,7 +541,7 @@
 fun find_subst sg T =
 let fun find (thm::thms) =
         let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
-            val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
+            val [P] = OldTerm.add_term_vars(concl_of thm,[]) \\ [va,vb]
             val eqT::_ = binder_types cT
         in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
            else find thms
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Import/proof_kernel.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen), Steven Obua
+    Author:     Sebastian Skalberg and Steven Obua, TU Muenchen
 *)
 
 signature ProofKernel =
@@ -1149,7 +1148,7 @@
       val ct = cprop_of thm
       val t = term_of ct
       val thy = theory_of_cterm ct
-      val frees = term_frees t
+      val frees = OldTerm.term_frees t
       val freenames = add_term_free_names (t, [])
       fun is_old_name n = n mem_string freenames
       fun name_of (Free (n, _)) = n
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Import/shuffler.ML
-    ID:         $Id$
     Author:     Sebastian Skalberg, TU Muenchen
 
 Package for proving two terms equal by normalizing (hence the
@@ -520,7 +519,7 @@
     let
         val thy = Thm.theory_of_thm th
         val c = prop_of th
-        val vars = add_term_frees (c,add_term_vars(c,[]))
+        val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
     in
         Drule.forall_intr_list (map (cterm_of thy) vars) th
     end
@@ -585,7 +584,7 @@
 
 fun set_prop thy t =
     let
-        val vars = add_term_frees (t,add_term_vars (t,[]))
+        val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
         val closed_t = fold_rev Logic.all vars t
         val rew_th = norm_term thy closed_t
         val rhs = Thm.rhs_of rew_th
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Library/comm_ring.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
-(*  ID:         $Id$
-    Author:     Amine Chaieb
+(*  Author:     Amine Chaieb
 
 Tactic for solving equalities over commutative rings.
 *)
@@ -71,7 +70,7 @@
 fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
       if Sign.of_sort thy (T, cr_sort) then
         let
-          val fs = term_frees eq;
+          val fs = OldTerm.term_frees eq;
           val cvs = cterm_of thy (HOLogic.mk_list T fs);
           val clhs = cterm_of thy (reif_polex T fs lhs);
           val crhs = cterm_of thy (reif_polex T fs rhs);
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,3 @@
-
-(* $Id$ *)
 
 val trace_mc = ref false; 
 
@@ -250,7 +248,7 @@
    and thm.instantiate *)
 fun freeze_thaw t =
   let val used = add_term_names (t, [])
-          and vars = term_vars t;
+          and vars = OldTerm.term_vars t;
       fun newName (Var(ix,_), (pairs,used)) = 
           let val v = Name.variant used (string_of_indexname ix)
           in  ((ix,v)::pairs, v::used)  end;
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,10 +1,8 @@
 (*  Title:      HOL/Nominal/nominal_fresh_fun.ML
-    ID:         $Id$
-    Authors:    Stefan Berghofer, Julien Narboux, TU Muenchen
+    Authors:    Stefan Berghofer and Julien Narboux, TU Muenchen
 
 Provides a tactic to generate fresh names and
 a tactic to analyse instances of the fresh_fun.
-
 *)
 
 (* First some functions that should be in the library *)
@@ -83,7 +81,7 @@
    val bvs = map_index (Bound o fst) ps;
 (* select variables of the right class *)
    val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
-     (term_frees goal @ bvs);
+     (OldTerm.term_frees goal @ bvs);
 (* build the tuple *)
    val s = (Library.foldr1 (fn (v, s) =>
      HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;  (* FIXME avoid handle _ *)
@@ -91,7 +89,7 @@
    val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
 (* find the variable we want to instantiate *)
-   val x = hd (term_vars (prop_of exists_fresh'));
+   val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
  in 
    (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    rtac fs_name_thm 1 THEN
@@ -150,7 +148,7 @@
     val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
     val ss' = ss addsimps fresh_prod::abs_fresh;
     val ss'' = ss' addsimps fresh_perm_app;
-    val x = hd (tl (term_vars (prop_of exI)));
+    val x = hd (tl (OldTerm.term_vars (prop_of exI)));
     val goal = nth (prems_of thm) (i-1);
     val atom_name_opt = get_inner_fresh_fun goal;
     val n = List.length (Logic.strip_params goal);
@@ -165,7 +163,7 @@
     val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
     val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
     fun inst_fresh vars params i st =
-   let val vars' = term_vars (prop_of st);
+   let val vars' = OldTerm.term_vars (prop_of st);
        val thy = theory_of_thm st;
    in case vars' \\ vars of 
      [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
@@ -174,7 +172,7 @@
   in
   ((fn st =>
   let 
-    val vars = term_vars (prop_of st);
+    val vars = OldTerm.term_vars (prop_of st);
     val params = Logic.strip_params (nth (prems_of st) (i-1))
     (* The tactics which solve the subgoals generated 
        by the conditionnal rewrite rule. *)
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Nominal/nominal_inductive.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Infrastructure for proving equivariance and strong induction theorems
@@ -238,7 +237,7 @@
         val prem = Logic.list_implies
           (map mk_fresh bvars @ mk_distinct bvars @
            map (fn prem =>
-             if null (term_frees prem inter ps) then prem
+             if null (OldTerm.term_frees prem inter ps) then prem
              else lift_prem prem) prems,
            HOLogic.mk_Trueprop (lift_pred p ts));
         val vs = map (Var o apfst (rpair 0)) (rename_wrt_term prem params')
@@ -264,7 +263,7 @@
     val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
       map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
           (List.mapPartial (fn prem =>
-             if null (ps inter term_frees prem) then SOME prem
+             if null (ps inter OldTerm.term_frees prem) then SOME prem
              else map_term (split_conj (K o I) names) prem prem) prems, q))))
         (mk_distinct bvars @
          maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
@@ -353,7 +352,7 @@
                          (rev pis' @ pis) th));
                  val (gprems1, gprems2) = split_list
                    (map (fn (th, t) =>
-                      if null (term_frees t inter ps) then (SOME th, mk_pi th)
+                      if null (OldTerm.term_frees t inter ps) then (SOME th, mk_pi th)
                       else
                         (map_thm ctxt (split_conj (K o I) names)
                            (etac conjunct1 1) monos NONE th,
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Nominal/nominal_inductive2.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Infrastructure for proving equivariance and strong induction theorems
@@ -254,7 +253,7 @@
         val prem = Logic.list_implies
           (map mk_fresh sets @
            map (fn prem =>
-             if null (term_frees prem inter ps) then prem
+             if null (OldTerm.term_frees prem inter ps) then prem
              else lift_prem prem) prems,
            HOLogic.mk_Trueprop (lift_pred p ts));
       in abs_params params' prem end) prems);
@@ -277,7 +276,7 @@
     val (vc_compat, vc_compat') = map (fn (params, sets, prems, (p, ts)) =>
       map (fn q => abs_params params (incr_boundvars ~1 (Logic.list_implies
           (List.mapPartial (fn prem =>
-             if null (ps inter term_frees prem) then SOME prem
+             if null (ps inter OldTerm.term_frees prem) then SOME prem
              else map_term (split_conj (K o I) names) prem prem) prems, q))))
         (maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
            (NominalPackage.fresh_star_const U T $ u $ t)) sets)
@@ -364,7 +363,7 @@
                    fold_rev (NominalPackage.mk_perm []) pis t) sets';
                  val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
                  val gprems1 = List.mapPartial (fn (th, t) =>
-                   if null (term_frees t inter ps) then SOME th
+                   if null (OldTerm.term_frees t inter ps) then SOME th
                    else
                      map_thm ctxt' (split_conj (K o I) names)
                        (etac conjunct1 1) monos NONE th)
@@ -406,7 +405,7 @@
                        (fold_rev (mk_perm_bool o cterm_of thy)
                          (pis' @ pis) th));
                  val gprems2 = map (fn (th, t) =>
-                   if null (term_frees t inter ps) then mk_pi th
+                   if null (OldTerm.term_frees t inter ps) then mk_pi th
                    else
                      mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
                        (inst_conj_all_tac (length pis'')) monos (SOME t) th)))
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Nominal/nominal_primrec.ML
-    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
+    Author:     Norbert Voelker, FernUni Hagen
+    Author:     Stefan Berghofer, TU Muenchen
 
 Package for defining functions on nominal datatypes by primitive recursion.
 Taken from HOL/Tools/primrec_package.ML
@@ -71,7 +72,7 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
+        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
           |> filter_out (is_fixed o fst));
       case AList.lookup (op =) rec_fns fname of
         NONE =>
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/Qelim/cooper.ML
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -515,7 +514,7 @@
   let val _ = ()
   in
    Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
-      (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
+      (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
       (cooperex_conv ctxt) p 
   end
   handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
@@ -637,7 +636,7 @@
   let
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
-    val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
+    val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   in
     Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
       HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/Qelim/langford.ML
--- a/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -114,7 +114,7 @@
       let val (yes,no) = partition f xs 
       in if f x then (x::yes,no) else (yes, x::no) end;
 
-fun contains x ct = member (op aconv) (term_frees (term_of ct)) (term_of x);
+fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
 
 fun is_eqx x eq = case term_of eq of
    Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/Qelim/presburger.ML
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -86,8 +85,8 @@
 in 
 fun is_relevant ctxt ct = 
  gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
- andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct))
- andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct));
+ andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
+ andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
 
 fun int_nat_terms ctxt ct =
  let 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/TFL/casesplit.ML
-    ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 A structure that defines a tactic to program case splits.
@@ -104,7 +103,7 @@
     end;
 
 (*
- val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
+ val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
 *)
 
 
@@ -122,7 +121,7 @@
       val abs_ct = ctermify abst;
       val free_ct = ctermify x;
 
-      val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
+      val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
 
       val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
       val (Pv, Dv, type_insts) =
@@ -170,7 +169,7 @@
       val subgoalth' = atomize_goals subgoalth;
       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
 
-      val freets = Term.term_frees gt;
+      val freets = OldTerm.term_frees gt;
       fun getter x =
           let val (n,ty) = Term.dest_Free x in
             (if vstr = n orelse vstr = Name.dest_skolem n
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,9 +1,7 @@
 (*  Title:      HOL/Tools/TFL/rules.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 
-Emulation of HOL inference rules for TFL
+Emulation of HOL inference rules for TFL.
 *)
 
 signature RULES =
@@ -173,7 +171,7 @@
  *---------------------------------------------------------------------------*)
 local val thy = Thm.theory_of_thm disjI1
       val prop = Thm.prop_of disjI1
-      val [P,Q] = term_vars prop
+      val [P,Q] = OldTerm.term_vars prop
       val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
 in
 fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
@@ -182,7 +180,7 @@
 
 local val thy = Thm.theory_of_thm disjI2
       val prop = Thm.prop_of disjI2
-      val [P,Q] = term_vars prop
+      val [P,Q] = OldTerm.term_vars prop
       val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
 in
 fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
@@ -278,7 +276,7 @@
 local (* this is fragile *)
       val thy = Thm.theory_of_thm spec
       val prop = Thm.prop_of spec
-      val x = hd (tl (term_vars prop))
+      val x = hd (tl (OldTerm.term_vars prop))
       val cTV = ctyp_of thy (type_of x)
       val gspec = forall_intr (cterm_of thy x) spec
 in
@@ -295,7 +293,7 @@
 (* Not optimized! Too complicated. *)
 local val thy = Thm.theory_of_thm allI
       val prop = Thm.prop_of allI
-      val [P] = add_term_vars (prop, [])
+      val [P] = OldTerm.add_term_vars (prop, [])
       fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
       fun ctm_theta s = map (fn (i, (_, tm2)) =>
                              let val ctm2 = cterm_of s tm2
@@ -325,7 +323,7 @@
    let val thy = Thm.theory_of_thm thm
        val prop = Thm.prop_of thm
        val tycheck = cterm_of thy
-       val vlist = map tycheck (add_term_vars (prop, []))
+       val vlist = map tycheck (OldTerm.add_term_vars (prop, []))
   in GENL vlist thm
   end;
 
@@ -365,7 +363,7 @@
 
 local val thy = Thm.theory_of_thm exI
       val prop = Thm.prop_of exI
-      val [P,x] = term_vars prop
+      val [P,x] = OldTerm.term_vars prop
 in
 fun EXISTS (template,witness) thm =
    let val thy = Thm.theory_of_thm thm
@@ -765,7 +763,7 @@
               val thy = Thm.theory_of_thm thm
               val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
               fun genl tm = let val vlist = subtract (op aconv) globals
-                                           (add_term_frees(tm,[]))
+                                           (OldTerm.add_term_frees(tm,[]))
                             in fold_rev Forall vlist tm
                             end
               (*--------------------------------------------------------------
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Tools/TFL/usyntax.ML
-    ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
-    Copyright   1997  University of Cambridge
 
 Emulation of HOL's abstract syntax functions.
 *)
@@ -321,7 +319,7 @@
 
 
 (* Need to reverse? *)
-fun gen_all tm = list_mk_forall(term_frees tm, tm);
+fun gen_all tm = list_mk_forall(OldTerm.term_frees tm, tm);
 
 (* Destructing a cterm to a list of Terms *)
 fun strip_comb tm =
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,8 +1,6 @@
 (*  Title:      HOL/Tools/cnf_funcs.ML
-    ID:         $Id$
     Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
-    Author:     Tjark Weber
-    Copyright   2005-2006
+    Author:     Tjark Weber, TU Muenchen
 
   FIXME: major overlaps with the code in meson.ML
 
@@ -499,7 +497,7 @@
 					NONE
 		in
 			Int.max (max, getOpt (idx, 0))
-		end) (term_frees simp) 0)
+		end) (OldTerm.term_frees simp) 0)
 	(* finally, convert to definitional CNF (this should preserve the simplification) *)
 	val cnfx_thm = make_cnfx_thm_from_nnf simp
 in
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/datatype_aux.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Auxiliary functions for defining datatypes.
@@ -131,7 +130,7 @@
     val flt = if null indnames then I else
       filter (fn Free (s, _) => s mem indnames | _ => false);
     fun abstr (t1, t2) = (case t1 of
-        NONE => (case flt (term_frees t2) of
+        NONE => (case flt (OldTerm.term_frees t2) of
             [Free (s, T)] => SOME (absfree (s, T, t2))
           | _ => NONE)
       | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/Tools/datatype_codegen.ML
-    ID:         $Id$
-    Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
+    Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
 
 Code generator facilities for inductive datatypes.
 *)
@@ -218,7 +217,7 @@
         val ts1 = Library.take (i, ts);
         val t :: ts2 = Library.drop (i, ts);
         val names = foldr add_term_names
-          (map (fst o fst o dest_Var) (foldr add_term_vars [] ts1)) ts1;
+          (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)));
 
         fun pcase [] [] [] gr = ([], gr)
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,12 +1,10 @@
 (*  Title:      HOL/Tools/function_package/context_tree.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions. 
 Builds and traverses trees of nested contexts along a term.
 *)
 
-
 signature FUNDEF_CTXTREE =
 sig
     type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *)
@@ -82,7 +80,7 @@
     let 
       val t' = snd (dest_all_all t)
       val (assumes, concl) = Logic.strip_horn t'
-    in (fold (curry add_term_vars) assumes [], term_vars concl)
+    in (fold (curry OldTerm.add_term_vars) assumes [], OldTerm.term_vars concl)
     end
 
 fun cong_deps crule =
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,9 +1,8 @@
 (*  Title:      HOL/Tools/function_package/fundef_core.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions.
-Main functionality
+A package for general recursive function definitions:
+Main functionality.
 *)
 
 signature FUNDEF_CORE =
@@ -437,7 +436,7 @@
                                   |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
                                   |> forall_intr (cterm_of thy x)
                                   |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
-                                  |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
+                                  |> (fn it => fold (forall_intr o cterm_of thy) (OldTerm.term_vars (prop_of it)) it)
 
         val goalstate =  Conjunction.intr graph_is_function complete
                           |> Thm.close_derivation
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/function_package/fundef_datatype.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
@@ -64,7 +63,7 @@
 
 fun inst_case_thm thy x P thm =
     let
-        val [Pv, xv] = term_vars (prop_of thm)
+        val [Pv, xv] = OldTerm.term_vars (prop_of thm)
     in
         cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
     end
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/inductive_codegen.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Code generator for inductive predicates.
@@ -129,7 +128,7 @@
   cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
     string_of_mode ms)) modes));
 
-val term_vs = map (fst o fst o dest_Var) o term_vars;
+val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
 val terms_vs = distinct (op =) o List.concat o (map term_vs);
 
 (** collect all Vars in a term (with duplicates!) **)
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,9 +1,8 @@
 (*  Title:      HOL/Tools/inductive_realizer.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Porgram extraction from proofs involving inductive predicates:
-Realizers for induction and elimination rules
+Realizers for induction and elimination rules.
 *)
 
 signature INDUCTIVE_REALIZER =
@@ -60,7 +59,7 @@
       (Var ((a, i), T), vs) => (case strip_type T of
         (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
       | _ => vs)
-    | (_, vs) => vs) [] (term_vars prop);
+    | (_, vs) => vs) [] (OldTerm.term_vars prop);
 
 fun dt_of_intrs thy vs nparms intrs =
   let
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -69,7 +69,7 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
+        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
           |> filter_out (is_fixed o fst));
       case AList.lookup (op =) rec_fns fname of
         NONE =>
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/record_package.ML
-    ID:         $Id$
     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
 
 Extensible records with structural subtyping in HOL.
@@ -934,7 +933,7 @@
                  then (let
                         val P=cterm_of thy (abstract_over_fun_app trm);
                         val thm = mk_fun_apply_eq trm thy;
-                        val PV = cterm_of thy (hd (term_vars (prop_of thm)));
+                        val PV = cterm_of thy (hd (OldTerm.term_vars (prop_of thm)));
                         val thm' = cterm_instantiate [(PV,P)] thm;
                        in SOME  thm' end handle TERM _ => NONE)
                 else NONE)
@@ -1305,7 +1304,7 @@
         | _ => false);
 
     val goal = nth (Thm.prems_of st) (i - 1);
-    val frees = List.filter (is_recT o type_of) (term_frees goal);
+    val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal);
 
     fun mk_split_free_tac free induct_thm i =
         let val cfree = cterm_of thy free;
@@ -1426,7 +1425,7 @@
           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
       | [x] => (head_of x, false));
     val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
-        [] => (case AList.lookup (op =) (map dest_Free (term_frees (prop_of st))) s of
+        [] => (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
           NONE => sys_error "try_param_tac: no such variable"
         | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl),
             (x, Free (s, T))])
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Tools/refute.ML
-    ID:         $Id$
-    Author:     Tjark Weber
-    Copyright   2003-2007
+    Author:     Tjark Weber, TU Muenchen
 
 Finite model generation for HOL formulas, using a SAT solver.
 *)
@@ -426,7 +424,7 @@
   fun close_form t =
   let
     (* (Term.indexname * Term.typ) list *)
-    val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
+    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
   in
     Library.foldl (fn (t', ((x, i), T)) =>
       (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
@@ -1294,7 +1292,7 @@
 
     (* existential closure over schematic variables *)
     (* (Term.indexname * Term.typ) list *)
-    val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
+    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
     (* Term.term *)
     val ex_closure = Library.foldl (fn (t', ((x, i), T)) =>
       (HOLogic.exists_const T) $
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,6 +1,4 @@
 (*  Author: Jia Meng, Cambridge University Computer Laboratory
-    ID: $Id$
-    Copyright 2004 University of Cambridge
 
 Transformation of axiom rules (elim/intro/etc) into CNF forms.
 *)
@@ -75,7 +73,7 @@
           (*Existential: declare a Skolem function, then insert into body and continue*)
           let
             val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
-            val args0 = term_frees xtp  (*get the formal parameter list*)
+            val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
             val Ts = map type_of args0
             val extraTs = rhs_extra_types (Ts ---> T) xtp
             val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
@@ -105,7 +103,7 @@
       fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
             (*Existential: declare a Skolem function, then insert into body and continue*)
             let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
-                val args = term_frees xtp \\ skos  (*the formal parameters*)
+                val args = OldTerm.term_frees xtp \\ skos  (*the formal parameters*)
                 val Ts = map type_of args
                 val cT = Ts ---> T
                 val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
@@ -158,9 +156,9 @@
 
 val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
 
-val [f_B,g_B] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S}));
 
 (*FIXME: requires more use of cterm constructors*)
 fun abstract ct =
@@ -495,8 +493,8 @@
       val defs = filter (is_absko o Thm.term_of) newhyps
       val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
                                       (map Thm.term_of hyps)
-      val fixed = term_frees (concl_of st) @
-                  foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
+      val fixed = OldTerm.term_frees (concl_of st) @
+                  foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
   in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
 
 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/specification_package.ML
-    ID:         $Id$
     Author:     Sebastian Skalberg, TU Muenchen
 
 Package for defining constants by specification.
@@ -118,7 +117,7 @@
 
         fun proc_single prop =
             let
-                val frees = Term.term_frees prop
+                val frees = OldTerm.term_frees prop
                 val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
                   orelse error "Specificaton: Only free variables of sort 'type' allowed"
                 val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/split_rule.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
 
 Some tools for managing tupled arguments and abstractions in rules.
@@ -105,7 +104,7 @@
 
 (*curries ALL function variables occurring in a rule's conclusion*)
 fun split_rule rl =
-  fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl
+  fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
   |> remove_internal_split
   |> Drule.standard;
 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/ex/MIR.thy
--- a/src/HOL/ex/MIR.thy	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/ex/MIR.thy	Wed Dec 31 00:08:13 2008 +0100
@@ -5899,7 +5899,7 @@
   let 
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
-    val fs = term_frees t;
+    val fs = OldTerm.term_frees t;
     val vs = fs ~~ (0 upto (length fs - 1));
     val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
     val t' = (term_of_fm vs o qe o fm_of_term vs) t;
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/ex/ReflectedFerrack.thy
--- a/src/HOL/ex/ReflectedFerrack.thy	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/ex/ReflectedFerrack.thy	Wed Dec 31 00:08:13 2008 +0100
@@ -1,4 +1,4 @@
-(*  Title:      Complex/ex/ReflectedFerrack.thy
+(*  Title:      HOL/ex/ReflectedFerrack.thy
     Author:     Amine Chaieb
 *)
 
@@ -2070,7 +2070,7 @@
   let 
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
-    val fs = term_frees t;
+    val fs = OldTerm.term_frees t;
     val vs = fs ~~ (0 upto (length fs - 1));
     val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
   in Thm.cterm_of thy res end
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Dec 31 00:08:13 2008 +0100
@@ -2039,7 +2039,7 @@
   let
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
-    val fs = term_frees t;
+    val fs = OldTerm.term_frees t;
     val bs = term_bools [] t;
     val vs = fs ~~ (0 upto (length fs - 1))
     val ps = bs ~~ (0 upto (length bs - 1))
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/ex/coopertac.ML
--- a/src/HOL/ex/coopertac.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/ex/coopertac.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -47,7 +47,7 @@
     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
-      (term_frees fm' @ term_vars fm');
+      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
     val fm2 = foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/ex/linrtac.ML
--- a/src/HOL/ex/linrtac.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/ex/linrtac.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -54,7 +54,7 @@
     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
-      (term_frees fm' @ term_vars fm');
+      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
     val fm2 = foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/HOL/ex/mirtac.ML
--- a/src/HOL/ex/mirtac.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/ex/mirtac.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Complex/ex/mirtac.ML
-    ID:         $Id$
+(*  Title:      HOL/ex/mirtac.ML
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -74,7 +73,7 @@
     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
-      (term_frees fm' @ term_vars fm');
+      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
     val fm2 = foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Proof/extraction.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Extraction of programs from proofs.
@@ -739,7 +738,7 @@
            in
              thy'
              |> PureThy.store_thm (corr_name s vs,
-                  Thm.varifyT (funpow (length (term_vars corr_prop))
+                  Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
                     (Thm.forall_elim_var 0) (forall_intr_frees
                       (ProofChecker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Proof/reconstruct.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Reconstruction of partial proof terms.
@@ -291,7 +290,7 @@
     val (t, prf, cs, env, _) = make_constraints_cprf thy
       (Envir.empty (maxidx_proof cprf ~1)) cprf';
     val cs' = map (fn p => (true, p, op union
-        (pairself (map (fst o dest_Var) o term_vars) p)))
+        (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
       (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
     val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
     val env' = solve thy cs' env
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Pure/drule.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      Pure/drule.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
 
 Derived rules and other operations on theorems.
 *)
@@ -340,7 +338,7 @@
      val thy = Thm.theory_of_thm fth
      val {prop, tpairs, ...} = rep_thm fth
  in
-   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
        [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
      | vars =>
          let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
@@ -363,7 +361,7 @@
      val thy = Thm.theory_of_thm fth
      val {prop, tpairs, ...} = rep_thm fth
  in
-   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
        [] => (fth, fn x => x)
      | vars =>
          let fun newName (Var(ix,_), (pairs,used)) =
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Pure/proofterm.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/proofterm.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 LF style proof terms.
@@ -420,7 +419,7 @@
         SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
    map_filter (fn Var (ixnT as (_, T)) =>
      (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
-        SOME (ixnT, Free ("dummy", T))) (term_vars t)) t;
+        SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
 
 fun norm_proof env =
   let
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Pure/term.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/term.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   Cambridge University 1992
 
 Simply typed lambda-calculus: types, terms, and basic operations.
 *)
@@ -132,10 +131,6 @@
   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 rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   val show_question_marks: bool ref
 end;
@@ -1150,27 +1145,6 @@
 fun term_tvars t = add_term_tvars(t,[]);
 
 
-(** Frees and Vars **)
-
-(*Accumulates the Vars in the term, suppressing duplicates*)
-fun add_term_vars (t, vars: term list) = case t of
-    Var   _ => OrdList.insert term_ord t vars
-  | Abs (_,_,body) => add_term_vars(body,vars)
-  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
-  | _ => vars;
-
-fun term_vars t = add_term_vars(t,[]);
-
-(*Accumulates the Frees in the term, suppressing duplicates*)
-fun add_term_frees (t, frees: term list) = case t of
-    Free   _ => OrdList.insert term_ord t frees
-  | Abs (_,_,body) => add_term_frees(body,frees)
-  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
-  | _ => frees;
-
-fun term_frees t = add_term_frees(t,[]);
-
-
 (* dest abstraction *)
 
 fun dest_abs (x, T, body) =
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Tools/IsaPlanner/isand.ML
--- a/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/IsaPlanner/isand.ML
-    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 Natural Deduction tools.
@@ -220,7 +219,7 @@
    with "names" *)
 fun fix_vars_to_frees_in_terms names ts = 
     let 
-      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
+      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
       val Ns = List.foldr Term.add_term_names names ts;
       val (_,renamings) = 
           Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
@@ -259,7 +258,7 @@
       val ctermify = Thm.cterm_of sgn
       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       val prop = (Thm.prop_of th);
-      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
+      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars 
                                                [] (prop :: tpairs));
       val cfixes = 
           map_filter 
@@ -360,7 +359,7 @@
       val sgn = Thm.theory_of_thm th;
       val ctermify = Thm.cterm_of sgn;
 
-      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
+      val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
       val cfrees = map (ctermify o Free o lookupfree allfrees) vs
 
       val sgs = prems_of th;
@@ -420,7 +419,7 @@
     let
       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) (Term.term_vars t)
+      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
       val names = Term.add_term_names (t,varnames);
       val fvs = map Free 
                     (Name.variant_list names (map fst alls)
@@ -429,7 +428,7 @@
 
 fun fix_alls_term i t = 
     let 
-      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
+      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
       val names = Term.add_term_names (t,varnames);
       val gt = Logic.get_goal t i;
       val body = Term.strip_all_body gt;
diff -r 4ea3358fac3f -r 5b4247055bd7 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/IsaPlanner/rw_inst.ML
-    ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 Rewriting using a conditional meta-equality theorem which supports
@@ -143,9 +142,9 @@
                     (Library.union
                        (Term.term_tvars t, tyvs),
                      Library.union 
-                       (map Term.dest_Var (Term.term_vars t), vs))) 
+                       (map Term.dest_Var (OldTerm.term_vars t), vs))) 
                 (([],[]), rule_conds);
-      val termvars = map Term.dest_Var (Term.term_vars tgt); 
+      val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
       val vars_to_fix = Library.union (termvars, cond_vs);
       val (renamings, names2) = 
           foldr (fn (((n,i),ty), (vs, names')) => 
diff -r 4ea3358fac3f -r 5b4247055bd7 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,5 @@
 (*  Title:      ZF/Tools/inductive_package.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
 
 Fixedpoint definition module -- for Inductive/Coinductive Definitions
 
@@ -113,7 +111,7 @@
   fun fp_part intr = (*quantify over rule's free vars except parameters*)
     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
         val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
-        val exfrees = term_frees intr \\ rec_params
+        val exfrees = OldTerm.term_frees intr \\ rec_params
         val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
     in foldr FOLogic.mk_exists
              (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
@@ -304,7 +302,7 @@
 
      (*Make a premise of the induction rule.*)
      fun induct_prem ind_alist intr =
-       let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
+       let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
            val iprems = foldr (add_induct_prem ind_alist) []
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr