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