moved old add_term_vars, add_term_frees etc. to structure OldTerm;
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