moved old add_term_vars, add_term_frees etc. to structure OldTerm;
authorwenzelm
Wed Dec 31 00:08:13 2008 +0100 (2008-12-31)
changeset 292655b4247055bd7
parent 29264 4ea3358fac3f
child 29266 4a478f9d2847
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
src/FOLP/simp.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/comm_ring.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/split_rule.ML
src/HOL/ex/MIR.thy
src/HOL/ex/ReflectedFerrack.thy
src/HOL/ex/Reflected_Presburger.thy
src/HOL/ex/coopertac.ML
src/HOL/ex/linrtac.ML
src/HOL/ex/mirtac.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/drule.ML
src/Pure/proofterm.ML
src/Pure/term.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOLP/simp.ML	Wed Dec 31 00:08:11 2008 +0100
     1.2 +++ b/src/FOLP/simp.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      FOLP/simp
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      FOLP/simp.ML
     1.7      Author:     Tobias Nipkow
     1.8      Copyright   1993  University of Cambridge
     1.9  
    1.10 @@ -156,21 +155,21 @@
    1.11  (*ccs contains the names of the constants possessing congruence rules*)
    1.12  fun add_hidden_vars ccs =
    1.13    let fun add_hvars tm hvars = case tm of
    1.14 -              Abs(_,_,body) => add_term_vars(body,hvars)
    1.15 +              Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
    1.16              | _$_ => let val (f,args) = strip_comb tm 
    1.17                       in case f of
    1.18                              Const(c,T) => 
    1.19                                  if member (op =) ccs c
    1.20                                  then fold_rev add_hvars args hvars
    1.21 -                                else add_term_vars (tm, hvars)
    1.22 -                          | _ => add_term_vars (tm, hvars)
    1.23 +                                else OldTerm.add_term_vars (tm, hvars)
    1.24 +                          | _ => OldTerm.add_term_vars (tm, hvars)
    1.25                       end
    1.26              | _ => hvars;
    1.27    in add_hvars end;
    1.28  
    1.29  fun add_new_asm_vars new_asms =
    1.30      let fun itf (tm, at) vars =
    1.31 -                if at then vars else add_term_vars(tm,vars)
    1.32 +                if at then vars else OldTerm.add_term_vars(tm,vars)
    1.33          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
    1.34                  in if length(tml)=length(al)
    1.35                     then fold_rev itf (tml ~~ al) vars
    1.36 @@ -198,7 +197,7 @@
    1.37      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    1.38      fun it_asms asm hvars =
    1.39          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
    1.40 -        else add_term_frees(asm,hvars)
    1.41 +        else OldTerm.add_term_frees(asm,hvars)
    1.42      val hvars = fold_rev it_asms asms hvars
    1.43      val hvs = map (#1 o dest_Var) hvars
    1.44      val refl1_tac = refl_tac 1
    1.45 @@ -542,7 +541,7 @@
    1.46  fun find_subst sg T =
    1.47  let fun find (thm::thms) =
    1.48          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
    1.49 -            val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
    1.50 +            val [P] = OldTerm.add_term_vars(concl_of thm,[]) \\ [va,vb]
    1.51              val eqT::_ = binder_types cT
    1.52          in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
    1.53             else find thms
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 00:08:11 2008 +0100
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 00:08:13 2008 +0100
     2.3 @@ -1,6 +1,5 @@
     2.4  (*  Title:      HOL/Import/proof_kernel.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Sebastian Skalberg (TU Muenchen), Steven Obua
     2.7 +    Author:     Sebastian Skalberg and Steven Obua, TU Muenchen
     2.8  *)
     2.9  
    2.10  signature ProofKernel =
    2.11 @@ -1149,7 +1148,7 @@
    2.12        val ct = cprop_of thm
    2.13        val t = term_of ct
    2.14        val thy = theory_of_cterm ct
    2.15 -      val frees = term_frees t
    2.16 +      val frees = OldTerm.term_frees t
    2.17        val freenames = add_term_free_names (t, [])
    2.18        fun is_old_name n = n mem_string freenames
    2.19        fun name_of (Free (n, _)) = n
     3.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:11 2008 +0100
     3.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:13 2008 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Import/shuffler.ML
     3.5 -    ID:         $Id$
     3.6      Author:     Sebastian Skalberg, TU Muenchen
     3.7  
     3.8  Package for proving two terms equal by normalizing (hence the
     3.9 @@ -520,7 +519,7 @@
    3.10      let
    3.11          val thy = Thm.theory_of_thm th
    3.12          val c = prop_of th
    3.13 -        val vars = add_term_frees (c,add_term_vars(c,[]))
    3.14 +        val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
    3.15      in
    3.16          Drule.forall_intr_list (map (cterm_of thy) vars) th
    3.17      end
    3.18 @@ -585,7 +584,7 @@
    3.19  
    3.20  fun set_prop thy t =
    3.21      let
    3.22 -        val vars = add_term_frees (t,add_term_vars (t,[]))
    3.23 +        val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
    3.24          val closed_t = fold_rev Logic.all vars t
    3.25          val rew_th = norm_term thy closed_t
    3.26          val rhs = Thm.rhs_of rew_th
     4.1 --- a/src/HOL/Library/comm_ring.ML	Wed Dec 31 00:08:11 2008 +0100
     4.2 +++ b/src/HOL/Library/comm_ring.ML	Wed Dec 31 00:08:13 2008 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4 -(*  ID:         $Id$
     4.5 -    Author:     Amine Chaieb
     4.6 +(*  Author:     Amine Chaieb
     4.7  
     4.8  Tactic for solving equalities over commutative rings.
     4.9  *)
    4.10 @@ -71,7 +70,7 @@
    4.11  fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
    4.12        if Sign.of_sort thy (T, cr_sort) then
    4.13          let
    4.14 -          val fs = term_frees eq;
    4.15 +          val fs = OldTerm.term_frees eq;
    4.16            val cvs = cterm_of thy (HOLogic.mk_list T fs);
    4.17            val clhs = cterm_of thy (reif_polex T fs lhs);
    4.18            val crhs = cterm_of thy (reif_polex T fs rhs);
     5.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 00:08:11 2008 +0100
     5.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 00:08:13 2008 +0100
     5.3 @@ -1,5 +1,3 @@
     5.4 -
     5.5 -(* $Id$ *)
     5.6  
     5.7  val trace_mc = ref false; 
     5.8  
     5.9 @@ -250,7 +248,7 @@
    5.10     and thm.instantiate *)
    5.11  fun freeze_thaw t =
    5.12    let val used = add_term_names (t, [])
    5.13 -          and vars = term_vars t;
    5.14 +          and vars = OldTerm.term_vars t;
    5.15        fun newName (Var(ix,_), (pairs,used)) = 
    5.16            let val v = Name.variant used (string_of_indexname ix)
    5.17            in  ((ix,v)::pairs, v::used)  end;
     6.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Dec 31 00:08:11 2008 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Dec 31 00:08:13 2008 +0100
     6.3 @@ -1,10 +1,8 @@
     6.4  (*  Title:      HOL/Nominal/nominal_fresh_fun.ML
     6.5 -    ID:         $Id$
     6.6 -    Authors:    Stefan Berghofer, Julien Narboux, TU Muenchen
     6.7 +    Authors:    Stefan Berghofer and Julien Narboux, TU Muenchen
     6.8  
     6.9  Provides a tactic to generate fresh names and
    6.10  a tactic to analyse instances of the fresh_fun.
    6.11 -
    6.12  *)
    6.13  
    6.14  (* First some functions that should be in the library *)
    6.15 @@ -83,7 +81,7 @@
    6.16     val bvs = map_index (Bound o fst) ps;
    6.17  (* select variables of the right class *)
    6.18     val vs = filter (fn t => is_of_fs_name (fastype_of1 (Ts, t)))
    6.19 -     (term_frees goal @ bvs);
    6.20 +     (OldTerm.term_frees goal @ bvs);
    6.21  (* build the tuple *)
    6.22     val s = (Library.foldr1 (fn (v, s) =>
    6.23       HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s) vs) handle _ => HOLogic.unit ;  (* FIXME avoid handle _ *)
    6.24 @@ -91,7 +89,7 @@
    6.25     val at_name_inst_thm = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    6.26     val exists_fresh' = at_name_inst_thm RS at_exists_fresh';
    6.27  (* find the variable we want to instantiate *)
    6.28 -   val x = hd (term_vars (prop_of exists_fresh'));
    6.29 +   val x = hd (OldTerm.term_vars (prop_of exists_fresh'));
    6.30   in 
    6.31     (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    6.32     rtac fs_name_thm 1 THEN
    6.33 @@ -150,7 +148,7 @@
    6.34      val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
    6.35      val ss' = ss addsimps fresh_prod::abs_fresh;
    6.36      val ss'' = ss' addsimps fresh_perm_app;
    6.37 -    val x = hd (tl (term_vars (prop_of exI)));
    6.38 +    val x = hd (tl (OldTerm.term_vars (prop_of exI)));
    6.39      val goal = nth (prems_of thm) (i-1);
    6.40      val atom_name_opt = get_inner_fresh_fun goal;
    6.41      val n = List.length (Logic.strip_params goal);
    6.42 @@ -165,7 +163,7 @@
    6.43      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    6.44      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    6.45      fun inst_fresh vars params i st =
    6.46 -   let val vars' = term_vars (prop_of st);
    6.47 +   let val vars' = OldTerm.term_vars (prop_of st);
    6.48         val thy = theory_of_thm st;
    6.49     in case vars' \\ vars of 
    6.50       [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    6.51 @@ -174,7 +172,7 @@
    6.52    in
    6.53    ((fn st =>
    6.54    let 
    6.55 -    val vars = term_vars (prop_of st);
    6.56 +    val vars = OldTerm.term_vars (prop_of st);
    6.57      val params = Logic.strip_params (nth (prems_of st) (i-1))
    6.58      (* The tactics which solve the subgoals generated 
    6.59         by the conditionnal rewrite rule. *)
     7.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 00:08:11 2008 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 00:08:13 2008 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/Nominal/nominal_inductive.ML
     7.5 -    ID:         $Id$
     7.6      Author:     Stefan Berghofer, TU Muenchen
     7.7  
     7.8  Infrastructure for proving equivariance and strong induction theorems
     7.9 @@ -238,7 +237,7 @@
    7.10          val prem = Logic.list_implies
    7.11            (map mk_fresh bvars @ mk_distinct bvars @
    7.12             map (fn prem =>
    7.13 -             if null (term_frees prem inter ps) then prem
    7.14 +             if null (OldTerm.term_frees prem inter ps) then prem
    7.15               else lift_prem prem) prems,
    7.16             HOLogic.mk_Trueprop (lift_pred p ts));
    7.17          val vs = map (Var o apfst (rpair 0)) (rename_wrt_term prem params')
    7.18 @@ -264,7 +263,7 @@
    7.19      val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
    7.20        map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
    7.21            (List.mapPartial (fn prem =>
    7.22 -             if null (ps inter term_frees prem) then SOME prem
    7.23 +             if null (ps inter OldTerm.term_frees prem) then SOME prem
    7.24               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    7.25          (mk_distinct bvars @
    7.26           maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    7.27 @@ -353,7 +352,7 @@
    7.28                           (rev pis' @ pis) th));
    7.29                   val (gprems1, gprems2) = split_list
    7.30                     (map (fn (th, t) =>
    7.31 -                      if null (term_frees t inter ps) then (SOME th, mk_pi th)
    7.32 +                      if null (OldTerm.term_frees t inter ps) then (SOME th, mk_pi th)
    7.33                        else
    7.34                          (map_thm ctxt (split_conj (K o I) names)
    7.35                             (etac conjunct1 1) monos NONE th,
     8.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 00:08:11 2008 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 00:08:13 2008 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOL/Nominal/nominal_inductive2.ML
     8.5 -    ID:         $Id$
     8.6      Author:     Stefan Berghofer, TU Muenchen
     8.7  
     8.8  Infrastructure for proving equivariance and strong induction theorems
     8.9 @@ -254,7 +253,7 @@
    8.10          val prem = Logic.list_implies
    8.11            (map mk_fresh sets @
    8.12             map (fn prem =>
    8.13 -             if null (term_frees prem inter ps) then prem
    8.14 +             if null (OldTerm.term_frees prem inter ps) then prem
    8.15               else lift_prem prem) prems,
    8.16             HOLogic.mk_Trueprop (lift_pred p ts));
    8.17        in abs_params params' prem end) prems);
    8.18 @@ -277,7 +276,7 @@
    8.19      val (vc_compat, vc_compat') = map (fn (params, sets, prems, (p, ts)) =>
    8.20        map (fn q => abs_params params (incr_boundvars ~1 (Logic.list_implies
    8.21            (List.mapPartial (fn prem =>
    8.22 -             if null (ps inter term_frees prem) then SOME prem
    8.23 +             if null (ps inter OldTerm.term_frees prem) then SOME prem
    8.24               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    8.25          (maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    8.26             (NominalPackage.fresh_star_const U T $ u $ t)) sets)
    8.27 @@ -364,7 +363,7 @@
    8.28                     fold_rev (NominalPackage.mk_perm []) pis t) sets';
    8.29                   val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
    8.30                   val gprems1 = List.mapPartial (fn (th, t) =>
    8.31 -                   if null (term_frees t inter ps) then SOME th
    8.32 +                   if null (OldTerm.term_frees t inter ps) then SOME th
    8.33                     else
    8.34                       map_thm ctxt' (split_conj (K o I) names)
    8.35                         (etac conjunct1 1) monos NONE th)
    8.36 @@ -406,7 +405,7 @@
    8.37                         (fold_rev (mk_perm_bool o cterm_of thy)
    8.38                           (pis' @ pis) th));
    8.39                   val gprems2 = map (fn (th, t) =>
    8.40 -                   if null (term_frees t inter ps) then mk_pi th
    8.41 +                   if null (OldTerm.term_frees t inter ps) then mk_pi th
    8.42                     else
    8.43                       mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
    8.44                         (inst_conj_all_tac (length pis'')) monos (SOME t) th)))
     9.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 00:08:11 2008 +0100
     9.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 00:08:13 2008 +0100
     9.3 @@ -1,5 +1,6 @@
     9.4  (*  Title:      HOL/Nominal/nominal_primrec.ML
     9.5 -    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
     9.6 +    Author:     Norbert Voelker, FernUni Hagen
     9.7 +    Author:     Stefan Berghofer, TU Muenchen
     9.8  
     9.9  Package for defining functions on nominal datatypes by primitive recursion.
    9.10  Taken from HOL/Tools/primrec_package.ML
    9.11 @@ -71,7 +72,7 @@
    9.12      else
    9.13       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    9.14        check_vars "extra variables on rhs: "
    9.15 -        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
    9.16 +        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
    9.17            |> filter_out (is_fixed o fst));
    9.18        case AList.lookup (op =) rec_fns fname of
    9.19          NONE =>
    10.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Dec 31 00:08:11 2008 +0100
    10.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Dec 31 00:08:13 2008 +0100
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Tools/Qelim/cooper.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Amine Chaieb, TU Muenchen
    10.7  *)
    10.8  
    10.9 @@ -515,7 +514,7 @@
   10.10    let val _ = ()
   10.11    in
   10.12     Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) 
   10.13 -      (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
   10.14 +      (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) 
   10.15        (cooperex_conv ctxt) p 
   10.16    end
   10.17    handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
   10.18 @@ -637,7 +636,7 @@
   10.19    let
   10.20      val thy = Thm.theory_of_cterm ct;
   10.21      val t = Thm.term_of ct;
   10.22 -    val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
   10.23 +    val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
   10.24    in
   10.25      Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
   10.26        HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
    11.1 --- a/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 00:08:11 2008 +0100
    11.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Wed Dec 31 00:08:13 2008 +0100
    11.3 @@ -114,7 +114,7 @@
    11.4        let val (yes,no) = partition f xs 
    11.5        in if f x then (x::yes,no) else (yes, x::no) end;
    11.6  
    11.7 -fun contains x ct = member (op aconv) (term_frees (term_of ct)) (term_of x);
    11.8 +fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
    11.9  
   11.10  fun is_eqx x eq = case term_of eq of
   11.11     Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
    12.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 00:08:11 2008 +0100
    12.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Dec 31 00:08:13 2008 +0100
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      HOL/Tools/Qelim/presburger.ML
    12.5 -    ID:         $Id$
    12.6      Author:     Amine Chaieb, TU Muenchen
    12.7  *)
    12.8  
    12.9 @@ -86,8 +85,8 @@
   12.10  in 
   12.11  fun is_relevant ctxt ct = 
   12.12   gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
   12.13 - andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct))
   12.14 - andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct));
   12.15 + andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
   12.16 + andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
   12.17  
   12.18  fun int_nat_terms ctxt ct =
   12.19   let 
    13.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 00:08:11 2008 +0100
    13.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Dec 31 00:08:13 2008 +0100
    13.3 @@ -1,5 +1,4 @@
    13.4  (*  Title:      HOL/Tools/TFL/casesplit.ML
    13.5 -    ID:         $Id$
    13.6      Author:     Lucas Dixon, University of Edinburgh
    13.7  
    13.8  A structure that defines a tactic to program case splits.
    13.9 @@ -104,7 +103,7 @@
   13.10      end;
   13.11  
   13.12  (*
   13.13 - val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;
   13.14 + val ty = (snd o hd o map Term.dest_Free o OldTerm.term_frees) t;
   13.15  *)
   13.16  
   13.17  
   13.18 @@ -122,7 +121,7 @@
   13.19        val abs_ct = ctermify abst;
   13.20        val free_ct = ctermify x;
   13.21  
   13.22 -      val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
   13.23 +      val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
   13.24  
   13.25        val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
   13.26        val (Pv, Dv, type_insts) =
   13.27 @@ -170,7 +169,7 @@
   13.28        val subgoalth' = atomize_goals subgoalth;
   13.29        val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
   13.30  
   13.31 -      val freets = Term.term_frees gt;
   13.32 +      val freets = OldTerm.term_frees gt;
   13.33        fun getter x =
   13.34            let val (n,ty) = Term.dest_Free x in
   13.35              (if vstr = n orelse vstr = Name.dest_skolem n
    14.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 00:08:11 2008 +0100
    14.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Dec 31 00:08:13 2008 +0100
    14.3 @@ -1,9 +1,7 @@
    14.4  (*  Title:      HOL/Tools/TFL/rules.ML
    14.5 -    ID:         $Id$
    14.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    14.7 -    Copyright   1997  University of Cambridge
    14.8  
    14.9 -Emulation of HOL inference rules for TFL
   14.10 +Emulation of HOL inference rules for TFL.
   14.11  *)
   14.12  
   14.13  signature RULES =
   14.14 @@ -173,7 +171,7 @@
   14.15   *---------------------------------------------------------------------------*)
   14.16  local val thy = Thm.theory_of_thm disjI1
   14.17        val prop = Thm.prop_of disjI1
   14.18 -      val [P,Q] = term_vars prop
   14.19 +      val [P,Q] = OldTerm.term_vars prop
   14.20        val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
   14.21  in
   14.22  fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
   14.23 @@ -182,7 +180,7 @@
   14.24  
   14.25  local val thy = Thm.theory_of_thm disjI2
   14.26        val prop = Thm.prop_of disjI2
   14.27 -      val [P,Q] = term_vars prop
   14.28 +      val [P,Q] = OldTerm.term_vars prop
   14.29        val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
   14.30  in
   14.31  fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
   14.32 @@ -278,7 +276,7 @@
   14.33  local (* this is fragile *)
   14.34        val thy = Thm.theory_of_thm spec
   14.35        val prop = Thm.prop_of spec
   14.36 -      val x = hd (tl (term_vars prop))
   14.37 +      val x = hd (tl (OldTerm.term_vars prop))
   14.38        val cTV = ctyp_of thy (type_of x)
   14.39        val gspec = forall_intr (cterm_of thy x) spec
   14.40  in
   14.41 @@ -295,7 +293,7 @@
   14.42  (* Not optimized! Too complicated. *)
   14.43  local val thy = Thm.theory_of_thm allI
   14.44        val prop = Thm.prop_of allI
   14.45 -      val [P] = add_term_vars (prop, [])
   14.46 +      val [P] = OldTerm.add_term_vars (prop, [])
   14.47        fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
   14.48        fun ctm_theta s = map (fn (i, (_, tm2)) =>
   14.49                               let val ctm2 = cterm_of s tm2
   14.50 @@ -325,7 +323,7 @@
   14.51     let val thy = Thm.theory_of_thm thm
   14.52         val prop = Thm.prop_of thm
   14.53         val tycheck = cterm_of thy
   14.54 -       val vlist = map tycheck (add_term_vars (prop, []))
   14.55 +       val vlist = map tycheck (OldTerm.add_term_vars (prop, []))
   14.56    in GENL vlist thm
   14.57    end;
   14.58  
   14.59 @@ -365,7 +363,7 @@
   14.60  
   14.61  local val thy = Thm.theory_of_thm exI
   14.62        val prop = Thm.prop_of exI
   14.63 -      val [P,x] = term_vars prop
   14.64 +      val [P,x] = OldTerm.term_vars prop
   14.65  in
   14.66  fun EXISTS (template,witness) thm =
   14.67     let val thy = Thm.theory_of_thm thm
   14.68 @@ -765,7 +763,7 @@
   14.69                val thy = Thm.theory_of_thm thm
   14.70                val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
   14.71                fun genl tm = let val vlist = subtract (op aconv) globals
   14.72 -                                           (add_term_frees(tm,[]))
   14.73 +                                           (OldTerm.add_term_frees(tm,[]))
   14.74                              in fold_rev Forall vlist tm
   14.75                              end
   14.76                (*--------------------------------------------------------------
    15.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 00:08:11 2008 +0100
    15.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Wed Dec 31 00:08:13 2008 +0100
    15.3 @@ -1,7 +1,5 @@
    15.4  (*  Title:      HOL/Tools/TFL/usyntax.ML
    15.5 -    ID:         $Id$
    15.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    15.7 -    Copyright   1997  University of Cambridge
    15.8  
    15.9  Emulation of HOL's abstract syntax functions.
   15.10  *)
   15.11 @@ -321,7 +319,7 @@
   15.12  
   15.13  
   15.14  (* Need to reverse? *)
   15.15 -fun gen_all tm = list_mk_forall(term_frees tm, tm);
   15.16 +fun gen_all tm = list_mk_forall(OldTerm.term_frees tm, tm);
   15.17  
   15.18  (* Destructing a cterm to a list of Terms *)
   15.19  fun strip_comb tm =
    16.1 --- a/src/HOL/Tools/cnf_funcs.ML	Wed Dec 31 00:08:11 2008 +0100
    16.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Wed Dec 31 00:08:13 2008 +0100
    16.3 @@ -1,8 +1,6 @@
    16.4  (*  Title:      HOL/Tools/cnf_funcs.ML
    16.5 -    ID:         $Id$
    16.6      Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
    16.7 -    Author:     Tjark Weber
    16.8 -    Copyright   2005-2006
    16.9 +    Author:     Tjark Weber, TU Muenchen
   16.10  
   16.11    FIXME: major overlaps with the code in meson.ML
   16.12  
   16.13 @@ -499,7 +497,7 @@
   16.14  					NONE
   16.15  		in
   16.16  			Int.max (max, getOpt (idx, 0))
   16.17 -		end) (term_frees simp) 0)
   16.18 +		end) (OldTerm.term_frees simp) 0)
   16.19  	(* finally, convert to definitional CNF (this should preserve the simplification) *)
   16.20  	val cnfx_thm = make_cnfx_thm_from_nnf simp
   16.21  in
    17.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Dec 31 00:08:11 2008 +0100
    17.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Dec 31 00:08:13 2008 +0100
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      HOL/Tools/datatype_aux.ML
    17.5 -    ID:         $Id$
    17.6      Author:     Stefan Berghofer, TU Muenchen
    17.7  
    17.8  Auxiliary functions for defining datatypes.
    17.9 @@ -131,7 +130,7 @@
   17.10      val flt = if null indnames then I else
   17.11        filter (fn Free (s, _) => s mem indnames | _ => false);
   17.12      fun abstr (t1, t2) = (case t1 of
   17.13 -        NONE => (case flt (term_frees t2) of
   17.14 +        NONE => (case flt (OldTerm.term_frees t2) of
   17.15              [Free (s, T)] => SOME (absfree (s, T, t2))
   17.16            | _ => NONE)
   17.17        | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
    18.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 00:08:11 2008 +0100
    18.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 31 00:08:13 2008 +0100
    18.3 @@ -1,6 +1,5 @@
    18.4  (*  Title:      HOL/Tools/datatype_codegen.ML
    18.5 -    ID:         $Id$
    18.6 -    Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
    18.7 +    Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
    18.8  
    18.9  Code generator facilities for inductive datatypes.
   18.10  *)
   18.11 @@ -218,7 +217,7 @@
   18.12          val ts1 = Library.take (i, ts);
   18.13          val t :: ts2 = Library.drop (i, ts);
   18.14          val names = foldr add_term_names
   18.15 -          (map (fst o fst o dest_Var) (foldr add_term_vars [] ts1)) ts1;
   18.16 +          (map (fst o fst o dest_Var) (foldr OldTerm.add_term_vars [] ts1)) ts1;
   18.17          val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
   18.18  
   18.19          fun pcase [] [] [] gr = ([], gr)
    19.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Wed Dec 31 00:08:11 2008 +0100
    19.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Dec 31 00:08:13 2008 +0100
    19.3 @@ -1,12 +1,10 @@
    19.4  (*  Title:      HOL/Tools/function_package/context_tree.ML
    19.5 -    ID:         $Id$
    19.6      Author:     Alexander Krauss, TU Muenchen
    19.7  
    19.8  A package for general recursive function definitions. 
    19.9  Builds and traverses trees of nested contexts along a term.
   19.10  *)
   19.11  
   19.12 -
   19.13  signature FUNDEF_CTXTREE =
   19.14  sig
   19.15      type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *)
   19.16 @@ -82,7 +80,7 @@
   19.17      let 
   19.18        val t' = snd (dest_all_all t)
   19.19        val (assumes, concl) = Logic.strip_horn t'
   19.20 -    in (fold (curry add_term_vars) assumes [], term_vars concl)
   19.21 +    in (fold (curry OldTerm.add_term_vars) assumes [], OldTerm.term_vars concl)
   19.22      end
   19.23  
   19.24  fun cong_deps crule =
    20.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Wed Dec 31 00:08:11 2008 +0100
    20.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Wed Dec 31 00:08:13 2008 +0100
    20.3 @@ -1,9 +1,8 @@
    20.4  (*  Title:      HOL/Tools/function_package/fundef_core.ML
    20.5 -    ID:         $Id$
    20.6      Author:     Alexander Krauss, TU Muenchen
    20.7  
    20.8 -A package for general recursive function definitions.
    20.9 -Main functionality
   20.10 +A package for general recursive function definitions:
   20.11 +Main functionality.
   20.12  *)
   20.13  
   20.14  signature FUNDEF_CORE =
   20.15 @@ -437,7 +436,7 @@
   20.16                                    |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
   20.17                                    |> forall_intr (cterm_of thy x)
   20.18                                    |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
   20.19 -                                  |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
   20.20 +                                  |> (fn it => fold (forall_intr o cterm_of thy) (OldTerm.term_vars (prop_of it)) it)
   20.21  
   20.22          val goalstate =  Conjunction.intr graph_is_function complete
   20.23                            |> Thm.close_derivation
    21.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Dec 31 00:08:11 2008 +0100
    21.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Dec 31 00:08:13 2008 +0100
    21.3 @@ -1,5 +1,4 @@
    21.4  (*  Title:      HOL/Tools/function_package/fundef_datatype.ML
    21.5 -    ID:         $Id$
    21.6      Author:     Alexander Krauss, TU Muenchen
    21.7  
    21.8  A package for general recursive function definitions.
    21.9 @@ -64,7 +63,7 @@
   21.10  
   21.11  fun inst_case_thm thy x P thm =
   21.12      let
   21.13 -        val [Pv, xv] = term_vars (prop_of thm)
   21.14 +        val [Pv, xv] = OldTerm.term_vars (prop_of thm)
   21.15      in
   21.16          cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
   21.17      end
    22.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 00:08:11 2008 +0100
    22.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Dec 31 00:08:13 2008 +0100
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOL/Tools/inductive_codegen.ML
    22.5 -    ID:         $Id$
    22.6      Author:     Stefan Berghofer, TU Muenchen
    22.7  
    22.8  Code generator for inductive predicates.
    22.9 @@ -129,7 +128,7 @@
   22.10    cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
   22.11      string_of_mode ms)) modes));
   22.12  
   22.13 -val term_vs = map (fst o fst o dest_Var) o term_vars;
   22.14 +val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
   22.15  val terms_vs = distinct (op =) o List.concat o (map term_vs);
   22.16  
   22.17  (** collect all Vars in a term (with duplicates!) **)
    23.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 00:08:11 2008 +0100
    23.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 00:08:13 2008 +0100
    23.3 @@ -1,9 +1,8 @@
    23.4  (*  Title:      HOL/Tools/inductive_realizer.ML
    23.5 -    ID:         $Id$
    23.6      Author:     Stefan Berghofer, TU Muenchen
    23.7  
    23.8  Porgram extraction from proofs involving inductive predicates:
    23.9 -Realizers for induction and elimination rules
   23.10 +Realizers for induction and elimination rules.
   23.11  *)
   23.12  
   23.13  signature INDUCTIVE_REALIZER =
   23.14 @@ -60,7 +59,7 @@
   23.15        (Var ((a, i), T), vs) => (case strip_type T of
   23.16          (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
   23.17        | _ => vs)
   23.18 -    | (_, vs) => vs) [] (term_vars prop);
   23.19 +    | (_, vs) => vs) [] (OldTerm.term_vars prop);
   23.20  
   23.21  fun dt_of_intrs thy vs nparms intrs =
   23.22    let
    24.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:11 2008 +0100
    24.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
    24.3 @@ -69,7 +69,7 @@
    24.4      else
    24.5       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    24.6        check_vars "extra variables on rhs: "
    24.7 -        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
    24.8 +        (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
    24.9            |> filter_out (is_fixed o fst));
   24.10        case AList.lookup (op =) rec_fns fname of
   24.11          NONE =>
    25.1 --- a/src/HOL/Tools/record_package.ML	Wed Dec 31 00:08:11 2008 +0100
    25.2 +++ b/src/HOL/Tools/record_package.ML	Wed Dec 31 00:08:13 2008 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:      HOL/Tools/record_package.ML
    25.5 -    ID:         $Id$
    25.6      Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
    25.7  
    25.8  Extensible records with structural subtyping in HOL.
    25.9 @@ -934,7 +933,7 @@
   25.10                   then (let
   25.11                          val P=cterm_of thy (abstract_over_fun_app trm);
   25.12                          val thm = mk_fun_apply_eq trm thy;
   25.13 -                        val PV = cterm_of thy (hd (term_vars (prop_of thm)));
   25.14 +                        val PV = cterm_of thy (hd (OldTerm.term_vars (prop_of thm)));
   25.15                          val thm' = cterm_instantiate [(PV,P)] thm;
   25.16                         in SOME  thm' end handle TERM _ => NONE)
   25.17                  else NONE)
   25.18 @@ -1305,7 +1304,7 @@
   25.19          | _ => false);
   25.20  
   25.21      val goal = nth (Thm.prems_of st) (i - 1);
   25.22 -    val frees = List.filter (is_recT o type_of) (term_frees goal);
   25.23 +    val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal);
   25.24  
   25.25      fun mk_split_free_tac free induct_thm i =
   25.26          let val cfree = cterm_of thy free;
   25.27 @@ -1426,7 +1425,7 @@
   25.28            (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
   25.29        | [x] => (head_of x, false));
   25.30      val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
   25.31 -        [] => (case AList.lookup (op =) (map dest_Free (term_frees (prop_of st))) s of
   25.32 +        [] => (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
   25.33            NONE => sys_error "try_param_tac: no such variable"
   25.34          | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl),
   25.35              (x, Free (s, T))])
    26.1 --- a/src/HOL/Tools/refute.ML	Wed Dec 31 00:08:11 2008 +0100
    26.2 +++ b/src/HOL/Tools/refute.ML	Wed Dec 31 00:08:13 2008 +0100
    26.3 @@ -1,7 +1,5 @@
    26.4  (*  Title:      HOL/Tools/refute.ML
    26.5 -    ID:         $Id$
    26.6 -    Author:     Tjark Weber
    26.7 -    Copyright   2003-2007
    26.8 +    Author:     Tjark Weber, TU Muenchen
    26.9  
   26.10  Finite model generation for HOL formulas, using a SAT solver.
   26.11  *)
   26.12 @@ -426,7 +424,7 @@
   26.13    fun close_form t =
   26.14    let
   26.15      (* (Term.indexname * Term.typ) list *)
   26.16 -    val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   26.17 +    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
   26.18    in
   26.19      Library.foldl (fn (t', ((x, i), T)) =>
   26.20        (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
   26.21 @@ -1294,7 +1292,7 @@
   26.22  
   26.23      (* existential closure over schematic variables *)
   26.24      (* (Term.indexname * Term.typ) list *)
   26.25 -    val vars = sort_wrt (fst o fst) (map dest_Var (term_vars t))
   26.26 +    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
   26.27      (* Term.term *)
   26.28      val ex_closure = Library.foldl (fn (t', ((x, i), T)) =>
   26.29        (HOLogic.exists_const T) $
    27.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Dec 31 00:08:11 2008 +0100
    27.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Dec 31 00:08:13 2008 +0100
    27.3 @@ -1,6 +1,4 @@
    27.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory
    27.5 -    ID: $Id$
    27.6 -    Copyright 2004 University of Cambridge
    27.7  
    27.8  Transformation of axiom rules (elim/intro/etc) into CNF forms.
    27.9  *)
   27.10 @@ -75,7 +73,7 @@
   27.11            (*Existential: declare a Skolem function, then insert into body and continue*)
   27.12            let
   27.13              val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
   27.14 -            val args0 = term_frees xtp  (*get the formal parameter list*)
   27.15 +            val args0 = OldTerm.term_frees xtp  (*get the formal parameter list*)
   27.16              val Ts = map type_of args0
   27.17              val extraTs = rhs_extra_types (Ts ---> T) xtp
   27.18              val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
   27.19 @@ -105,7 +103,7 @@
   27.20        fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
   27.21              (*Existential: declare a Skolem function, then insert into body and continue*)
   27.22              let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   27.23 -                val args = term_frees xtp \\ skos  (*the formal parameters*)
   27.24 +                val args = OldTerm.term_frees xtp \\ skos  (*the formal parameters*)
   27.25                  val Ts = map type_of args
   27.26                  val cT = Ts ---> T
   27.27                  val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
   27.28 @@ -158,9 +156,9 @@
   27.29  
   27.30  val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
   27.31  
   27.32 -val [f_B,g_B] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_B}));
   27.33 -val [g_C,f_C] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_C}));
   27.34 -val [f_S,g_S] = map (cterm_of (the_context ())) (term_vars (prop_of @{thm abs_S}));
   27.35 +val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B}));
   27.36 +val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C}));
   27.37 +val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S}));
   27.38  
   27.39  (*FIXME: requires more use of cterm constructors*)
   27.40  fun abstract ct =
   27.41 @@ -495,8 +493,8 @@
   27.42        val defs = filter (is_absko o Thm.term_of) newhyps
   27.43        val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
   27.44                                        (map Thm.term_of hyps)
   27.45 -      val fixed = term_frees (concl_of st) @
   27.46 -                  foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
   27.47 +      val fixed = OldTerm.term_frees (concl_of st) @
   27.48 +                  foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
   27.49    in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   27.50  
   27.51  
    28.1 --- a/src/HOL/Tools/specification_package.ML	Wed Dec 31 00:08:11 2008 +0100
    28.2 +++ b/src/HOL/Tools/specification_package.ML	Wed Dec 31 00:08:13 2008 +0100
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      HOL/Tools/specification_package.ML
    28.5 -    ID:         $Id$
    28.6      Author:     Sebastian Skalberg, TU Muenchen
    28.7  
    28.8  Package for defining constants by specification.
    28.9 @@ -118,7 +117,7 @@
   28.10  
   28.11          fun proc_single prop =
   28.12              let
   28.13 -                val frees = Term.term_frees prop
   28.14 +                val frees = OldTerm.term_frees prop
   28.15                  val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
   28.16                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
   28.17                  val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
    29.1 --- a/src/HOL/Tools/split_rule.ML	Wed Dec 31 00:08:11 2008 +0100
    29.2 +++ b/src/HOL/Tools/split_rule.ML	Wed Dec 31 00:08:13 2008 +0100
    29.3 @@ -1,5 +1,4 @@
    29.4  (*  Title:      HOL/Tools/split_rule.ML
    29.5 -    ID:         $Id$
    29.6      Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
    29.7  
    29.8  Some tools for managing tupled arguments and abstractions in rules.
    29.9 @@ -105,7 +104,7 @@
   29.10  
   29.11  (*curries ALL function variables occurring in a rule's conclusion*)
   29.12  fun split_rule rl =
   29.13 -  fold_rev split_rule_var' (Term.term_vars (concl_of rl)) rl
   29.14 +  fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
   29.15    |> remove_internal_split
   29.16    |> Drule.standard;
   29.17  
    30.1 --- a/src/HOL/ex/MIR.thy	Wed Dec 31 00:08:11 2008 +0100
    30.2 +++ b/src/HOL/ex/MIR.thy	Wed Dec 31 00:08:13 2008 +0100
    30.3 @@ -5899,7 +5899,7 @@
    30.4    let 
    30.5      val thy = Thm.theory_of_cterm ct;
    30.6      val t = Thm.term_of ct;
    30.7 -    val fs = term_frees t;
    30.8 +    val fs = OldTerm.term_frees t;
    30.9      val vs = fs ~~ (0 upto (length fs - 1));
   30.10      val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
   30.11      val t' = (term_of_fm vs o qe o fm_of_term vs) t;
    31.1 --- a/src/HOL/ex/ReflectedFerrack.thy	Wed Dec 31 00:08:11 2008 +0100
    31.2 +++ b/src/HOL/ex/ReflectedFerrack.thy	Wed Dec 31 00:08:13 2008 +0100
    31.3 @@ -1,4 +1,4 @@
    31.4 -(*  Title:      Complex/ex/ReflectedFerrack.thy
    31.5 +(*  Title:      HOL/ex/ReflectedFerrack.thy
    31.6      Author:     Amine Chaieb
    31.7  *)
    31.8  
    31.9 @@ -2070,7 +2070,7 @@
   31.10    let 
   31.11      val thy = Thm.theory_of_cterm ct;
   31.12      val t = Thm.term_of ct;
   31.13 -    val fs = term_frees t;
   31.14 +    val fs = OldTerm.term_frees t;
   31.15      val vs = fs ~~ (0 upto (length fs - 1));
   31.16      val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
   31.17    in Thm.cterm_of thy res end
    32.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Wed Dec 31 00:08:11 2008 +0100
    32.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Dec 31 00:08:13 2008 +0100
    32.3 @@ -2039,7 +2039,7 @@
    32.4    let
    32.5      val thy = Thm.theory_of_cterm ct;
    32.6      val t = Thm.term_of ct;
    32.7 -    val fs = term_frees t;
    32.8 +    val fs = OldTerm.term_frees t;
    32.9      val bs = term_bools [] t;
   32.10      val vs = fs ~~ (0 upto (length fs - 1))
   32.11      val ps = bs ~~ (0 upto (length bs - 1))
    33.1 --- a/src/HOL/ex/coopertac.ML	Wed Dec 31 00:08:11 2008 +0100
    33.2 +++ b/src/HOL/ex/coopertac.ML	Wed Dec 31 00:08:13 2008 +0100
    33.3 @@ -47,7 +47,7 @@
    33.4      val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    33.5        (foldr HOLogic.mk_imp c rhs, np) ps
    33.6      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
    33.7 -      (term_frees fm' @ term_vars fm');
    33.8 +      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
    33.9      val fm2 = foldr mk_all2 fm' vs
   33.10    in (fm2, np + length vs, length rhs) end;
   33.11  
    34.1 --- a/src/HOL/ex/linrtac.ML	Wed Dec 31 00:08:11 2008 +0100
    34.2 +++ b/src/HOL/ex/linrtac.ML	Wed Dec 31 00:08:13 2008 +0100
    34.3 @@ -54,7 +54,7 @@
    34.4      val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
    34.5        (foldr HOLogic.mk_imp c rhs, np) ps
    34.6      val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
    34.7 -      (term_frees fm' @ term_vars fm');
    34.8 +      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
    34.9      val fm2 = foldr mk_all2 fm' vs
   34.10    in (fm2, np + length vs, length rhs) end;
   34.11  
    35.1 --- a/src/HOL/ex/mirtac.ML	Wed Dec 31 00:08:11 2008 +0100
    35.2 +++ b/src/HOL/ex/mirtac.ML	Wed Dec 31 00:08:13 2008 +0100
    35.3 @@ -1,5 +1,4 @@
    35.4 -(*  Title:      HOL/Complex/ex/mirtac.ML
    35.5 -    ID:         $Id$
    35.6 +(*  Title:      HOL/ex/mirtac.ML
    35.7      Author:     Amine Chaieb, TU Muenchen
    35.8  *)
    35.9  
   35.10 @@ -74,7 +73,7 @@
   35.11      val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   35.12        (foldr HOLogic.mk_imp c rhs, np) ps
   35.13      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
   35.14 -      (term_frees fm' @ term_vars fm');
   35.15 +      (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
   35.16      val fm2 = foldr mk_all2 fm' vs
   35.17    in (fm2, np + length vs, length rhs) end;
   35.18  
    36.1 --- a/src/Pure/Proof/extraction.ML	Wed Dec 31 00:08:11 2008 +0100
    36.2 +++ b/src/Pure/Proof/extraction.ML	Wed Dec 31 00:08:13 2008 +0100
    36.3 @@ -1,5 +1,4 @@
    36.4  (*  Title:      Pure/Proof/extraction.ML
    36.5 -    ID:         $Id$
    36.6      Author:     Stefan Berghofer, TU Muenchen
    36.7  
    36.8  Extraction of programs from proofs.
    36.9 @@ -739,7 +738,7 @@
   36.10             in
   36.11               thy'
   36.12               |> PureThy.store_thm (corr_name s vs,
   36.13 -                  Thm.varifyT (funpow (length (term_vars corr_prop))
   36.14 +                  Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
   36.15                      (Thm.forall_elim_var 0) (forall_intr_frees
   36.16                        (ProofChecker.thm_of_proof thy'
   36.17                         (fst (Proofterm.freeze_thaw_prf prf))))))
    37.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Dec 31 00:08:11 2008 +0100
    37.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Dec 31 00:08:13 2008 +0100
    37.3 @@ -1,5 +1,4 @@
    37.4  (*  Title:      Pure/Proof/reconstruct.ML
    37.5 -    ID:         $Id$
    37.6      Author:     Stefan Berghofer, TU Muenchen
    37.7  
    37.8  Reconstruction of partial proof terms.
    37.9 @@ -291,7 +290,7 @@
   37.10      val (t, prf, cs, env, _) = make_constraints_cprf thy
   37.11        (Envir.empty (maxidx_proof cprf ~1)) cprf';
   37.12      val cs' = map (fn p => (true, p, op union
   37.13 -        (pairself (map (fst o dest_Var) o term_vars) p)))
   37.14 +        (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
   37.15        (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
   37.16      val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
   37.17      val env' = solve thy cs' env
    38.1 --- a/src/Pure/drule.ML	Wed Dec 31 00:08:11 2008 +0100
    38.2 +++ b/src/Pure/drule.ML	Wed Dec 31 00:08:13 2008 +0100
    38.3 @@ -1,7 +1,5 @@
    38.4  (*  Title:      Pure/drule.ML
    38.5 -    ID:         $Id$
    38.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    38.7 -    Copyright   1993  University of Cambridge
    38.8  
    38.9  Derived rules and other operations on theorems.
   38.10  *)
   38.11 @@ -340,7 +338,7 @@
   38.12       val thy = Thm.theory_of_thm fth
   38.13       val {prop, tpairs, ...} = rep_thm fth
   38.14   in
   38.15 -   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   38.16 +   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   38.17         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
   38.18       | vars =>
   38.19           let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
   38.20 @@ -363,7 +361,7 @@
   38.21       val thy = Thm.theory_of_thm fth
   38.22       val {prop, tpairs, ...} = rep_thm fth
   38.23   in
   38.24 -   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   38.25 +   case List.foldr OldTerm.add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   38.26         [] => (fth, fn x => x)
   38.27       | vars =>
   38.28           let fun newName (Var(ix,_), (pairs,used)) =
    39.1 --- a/src/Pure/proofterm.ML	Wed Dec 31 00:08:11 2008 +0100
    39.2 +++ b/src/Pure/proofterm.ML	Wed Dec 31 00:08:13 2008 +0100
    39.3 @@ -1,5 +1,4 @@
    39.4  (*  Title:      Pure/proofterm.ML
    39.5 -    ID:         $Id$
    39.6      Author:     Stefan Berghofer, TU Muenchen
    39.7  
    39.8  LF style proof terms.
    39.9 @@ -420,7 +419,7 @@
   39.10          SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
   39.11     map_filter (fn Var (ixnT as (_, T)) =>
   39.12       (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
   39.13 -        SOME (ixnT, Free ("dummy", T))) (term_vars t)) t;
   39.14 +        SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t;
   39.15  
   39.16  fun norm_proof env =
   39.17    let
    40.1 --- a/src/Pure/term.ML	Wed Dec 31 00:08:11 2008 +0100
    40.2 +++ b/src/Pure/term.ML	Wed Dec 31 00:08:13 2008 +0100
    40.3 @@ -1,6 +1,5 @@
    40.4  (*  Title:      Pure/term.ML
    40.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    40.6 -    Copyright   Cambridge University 1992
    40.7  
    40.8  Simply typed lambda-calculus: types, terms, and basic operations.
    40.9  *)
   40.10 @@ -132,10 +131,6 @@
   40.11    val typ_tvars: typ -> (indexname * sort) list
   40.12    val term_tfrees: term -> (string * sort) list
   40.13    val term_tvars: term -> (indexname * sort) list
   40.14 -  val add_term_vars: term * term list -> term list
   40.15 -  val term_vars: term -> term list
   40.16 -  val add_term_frees: term * term list -> term list
   40.17 -  val term_frees: term -> term list
   40.18    val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   40.19    val show_question_marks: bool ref
   40.20  end;
   40.21 @@ -1150,27 +1145,6 @@
   40.22  fun term_tvars t = add_term_tvars(t,[]);
   40.23  
   40.24  
   40.25 -(** Frees and Vars **)
   40.26 -
   40.27 -(*Accumulates the Vars in the term, suppressing duplicates*)
   40.28 -fun add_term_vars (t, vars: term list) = case t of
   40.29 -    Var   _ => OrdList.insert term_ord t vars
   40.30 -  | Abs (_,_,body) => add_term_vars(body,vars)
   40.31 -  | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   40.32 -  | _ => vars;
   40.33 -
   40.34 -fun term_vars t = add_term_vars(t,[]);
   40.35 -
   40.36 -(*Accumulates the Frees in the term, suppressing duplicates*)
   40.37 -fun add_term_frees (t, frees: term list) = case t of
   40.38 -    Free   _ => OrdList.insert term_ord t frees
   40.39 -  | Abs (_,_,body) => add_term_frees(body,frees)
   40.40 -  | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   40.41 -  | _ => frees;
   40.42 -
   40.43 -fun term_frees t = add_term_frees(t,[]);
   40.44 -
   40.45 -
   40.46  (* dest abstraction *)
   40.47  
   40.48  fun dest_abs (x, T, body) =
    41.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 00:08:11 2008 +0100
    41.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Dec 31 00:08:13 2008 +0100
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title:      Tools/IsaPlanner/isand.ML
    41.5 -    ID:		$Id$
    41.6      Author:     Lucas Dixon, University of Edinburgh
    41.7  
    41.8  Natural Deduction tools.
    41.9 @@ -220,7 +219,7 @@
   41.10     with "names" *)
   41.11  fun fix_vars_to_frees_in_terms names ts = 
   41.12      let 
   41.13 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
   41.14 +      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars [] ts);
   41.15        val Ns = List.foldr Term.add_term_names names ts;
   41.16        val (_,renamings) = 
   41.17            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   41.18 @@ -259,7 +258,7 @@
   41.19        val ctermify = Thm.cterm_of sgn
   41.20        val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   41.21        val prop = (Thm.prop_of th);
   41.22 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
   41.23 +      val vars = map Term.dest_Var (List.foldr OldTerm.add_term_vars 
   41.24                                                 [] (prop :: tpairs));
   41.25        val cfixes = 
   41.26            map_filter 
   41.27 @@ -360,7 +359,7 @@
   41.28        val sgn = Thm.theory_of_thm th;
   41.29        val ctermify = Thm.cterm_of sgn;
   41.30  
   41.31 -      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
   41.32 +      val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
   41.33        val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   41.34  
   41.35        val sgs = prems_of th;
   41.36 @@ -420,7 +419,7 @@
   41.37      let
   41.38        val t = Term.strip_all_body alledt;
   41.39        val alls = rev (Term.strip_all_vars alledt);
   41.40 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   41.41 +      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
   41.42        val names = Term.add_term_names (t,varnames);
   41.43        val fvs = map Free 
   41.44                      (Name.variant_list names (map fst alls)
   41.45 @@ -429,7 +428,7 @@
   41.46  
   41.47  fun fix_alls_term i t = 
   41.48      let 
   41.49 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   41.50 +      val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
   41.51        val names = Term.add_term_names (t,varnames);
   41.52        val gt = Logic.get_goal t i;
   41.53        val body = Term.strip_all_body gt;
    42.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 00:08:11 2008 +0100
    42.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Dec 31 00:08:13 2008 +0100
    42.3 @@ -1,5 +1,4 @@
    42.4  (*  Title:      Tools/IsaPlanner/rw_inst.ML
    42.5 -    ID:         $Id$
    42.6      Author:     Lucas Dixon, University of Edinburgh
    42.7  
    42.8  Rewriting using a conditional meta-equality theorem which supports
    42.9 @@ -143,9 +142,9 @@
   42.10                      (Library.union
   42.11                         (Term.term_tvars t, tyvs),
   42.12                       Library.union 
   42.13 -                       (map Term.dest_Var (Term.term_vars t), vs))) 
   42.14 +                       (map Term.dest_Var (OldTerm.term_vars t), vs))) 
   42.15                  (([],[]), rule_conds);
   42.16 -      val termvars = map Term.dest_Var (Term.term_vars tgt); 
   42.17 +      val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
   42.18        val vars_to_fix = Library.union (termvars, cond_vs);
   42.19        val (renamings, names2) = 
   42.20            foldr (fn (((n,i),ty), (vs, names')) => 
    43.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Dec 31 00:08:11 2008 +0100
    43.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Dec 31 00:08:13 2008 +0100
    43.3 @@ -1,7 +1,5 @@
    43.4  (*  Title:      ZF/Tools/inductive_package.ML
    43.5 -    ID:         $Id$
    43.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.7 -    Copyright   1994  University of Cambridge
    43.8  
    43.9  Fixedpoint definition module -- for Inductive/Coinductive Definitions
   43.10  
   43.11 @@ -113,7 +111,7 @@
   43.12    fun fp_part intr = (*quantify over rule's free vars except parameters*)
   43.13      let val prems = map dest_tprop (Logic.strip_imp_prems intr)
   43.14          val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
   43.15 -        val exfrees = term_frees intr \\ rec_params
   43.16 +        val exfrees = OldTerm.term_frees intr \\ rec_params
   43.17          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
   43.18      in foldr FOLogic.mk_exists
   43.19               (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
   43.20 @@ -304,7 +302,7 @@
   43.21  
   43.22       (*Make a premise of the induction rule.*)
   43.23       fun induct_prem ind_alist intr =
   43.24 -       let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
   43.25 +       let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
   43.26             val iprems = foldr (add_induct_prem ind_alist) []
   43.27                                (Logic.strip_imp_prems intr)
   43.28             val (t,X) = Ind_Syntax.rule_concl intr