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