--- a/src/FOL/IFOL.thy Wed Aug 10 20:12:36 2011 +0200
+++ b/src/FOL/IFOL.thy Wed Aug 10 20:53:43 2011 +0200
@@ -7,6 +7,7 @@
theory IFOL
imports Pure
uses
+ "~~/src/Tools/misc_legacy.ML"
"~~/src/Provers/splitter.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Tools/IsaPlanner/zipper.ML"
--- a/src/FOL/IsaMakefile Wed Aug 10 20:12:36 2011 +0200
+++ b/src/FOL/IsaMakefile Wed Aug 10 20:53:43 2011 +0200
@@ -29,8 +29,9 @@
$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Tools/case_product.ML $(SRC)/Tools/IsaPlanner/zipper.ML \
- $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+ $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML \
+ $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \
+ $(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \
$(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \
--- a/src/FOLP/IFOLP.thy Wed Aug 10 20:12:36 2011 +0200
+++ b/src/FOLP/IFOLP.thy Wed Aug 10 20:53:43 2011 +0200
@@ -7,7 +7,7 @@
theory IFOLP
imports Pure
-uses ("hypsubst.ML") ("intprover.ML")
+uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML")
begin
setup Pure_Thy.old_appl_syntax_setup
--- a/src/FOLP/IsaMakefile Wed Aug 10 20:12:36 2011 +0200
+++ b/src/FOLP/IsaMakefile Wed Aug 10 20:53:43 2011 +0200
@@ -26,7 +26,7 @@
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML \
- hypsubst.ML intprover.ML simp.ML simpdata.ML
+ hypsubst.ML intprover.ML simp.ML simpdata.ML $(SRC)/Tools/misc_legacy.ML
@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
--- a/src/FOLP/simp.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/FOLP/simp.ML Wed Aug 10 20:53:43 2011 +0200
@@ -155,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) => OldTerm.add_term_vars(body,hvars)
+ Abs(_,_,body) => Misc_Legacy.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 OldTerm.add_term_vars (tm, hvars)
- | _ => OldTerm.add_term_vars (tm, hvars)
+ else Misc_Legacy.add_term_vars (tm, hvars)
+ | _ => Misc_Legacy.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 OldTerm.add_term_vars(tm,vars)
+ if at then vars else Misc_Legacy.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
@@ -197,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 OldTerm.add_term_frees(asm,hvars)
+ else Misc_Legacy.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
@@ -543,7 +543,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] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
+ val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, []));
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/Decision_Procs/Cooper.thy Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Aug 10 20:53:43 2011 +0200
@@ -1996,7 +1996,7 @@
let
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
- val fs = OldTerm.term_frees t;
+ val fs = Misc_Legacy.term_frees t;
val bs = term_bools [] t;
val vs = map_index swap fs;
val ps = map_index swap bs;
--- a/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Aug 10 20:53:43 2011 +0200
@@ -5635,7 +5635,7 @@
let
val thy = Thm.theory_of_cterm ct;
val t = Thm.term_of ct;
- val fs = OldTerm.term_frees t;
+ val fs = Misc_Legacy.term_frees t;
val vs = map_index swap fs;
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/Decision_Procs/commutative_ring_tac.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Wed Aug 10 20:53:43 2011 +0200
@@ -68,7 +68,7 @@
fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) =
if Sign.of_sort thy (T, cr_sort) then
let
- val fs = OldTerm.term_frees eq;
+ val fs = Misc_Legacy.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/Decision_Procs/cooper_tac.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 10 20:53:43 2011 +0200
@@ -55,7 +55,7 @@
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
- (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
+ (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Aug 10 20:53:43 2011 +0200
@@ -61,7 +61,7 @@
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
- (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
+ (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
--- a/src/HOL/Decision_Procs/langford.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Wed Aug 10 20:53:43 2011 +0200
@@ -113,7 +113,7 @@
val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
-fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
+fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 10 20:53:43 2011 +0200
@@ -76,7 +76,7 @@
val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
(List.foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
- (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
+ (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm');
val fm2 = List.foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
--- a/src/HOL/HOL.thy Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/HOL.thy Wed Aug 10 20:53:43 2011 +0200
@@ -15,7 +15,6 @@
"~~/src/Tools/intuitionistic.ML"
"~~/src/Tools/project_rule.ML"
"~~/src/Tools/cong_tac.ML"
- "~~/src/Tools/misc_legacy.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Provers/splitter.ML"
"~~/src/Provers/classical.ML"
--- a/src/HOL/Import/proof_kernel.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Aug 10 20:53:43 2011 +0200
@@ -1059,7 +1059,7 @@
val ct = cprop_of thm
val t = term_of ct
val thy = theory_of_cterm ct
- val frees = OldTerm.term_frees t
+ val frees = Misc_Legacy.term_frees t
val freenames = Term.add_free_names t []
val is_old_name = member (op =) freenames
fun name_of (Free (n, _)) = n
@@ -1339,9 +1339,9 @@
let
val _ = message "INST_TYPE:"
val _ = if_debug pth hth
- val tys_before = OldTerm.add_term_tfrees (prop_of th,[])
+ val tys_before = Misc_Legacy.add_term_tfrees (prop_of th,[])
val th1 = Thm.varifyT_global th
- val tys_after = OldTerm.add_term_tvars (prop_of th1,[])
+ val tys_after = Misc_Legacy.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)
@@ -2002,7 +2002,7 @@
val c = case concl_of th2 of
_ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "new_type_definition" "Bad type definition theorem"
- val tfrees = OldTerm.term_tfrees c
+ val tfrees = Misc_Legacy.term_tfrees c
val tnames = map fst tfrees
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
@@ -2075,7 +2075,7 @@
val c = case concl_of th2 of
_ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
| _ => raise ERR "type_introduction" "Bad type definition theorem"
- val tfrees = OldTerm.term_tfrees c
+ val tfrees = Misc_Legacy.term_tfrees c
val tnames = sort_strings (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
--- a/src/HOL/Import/shuffler.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Import/shuffler.ML Wed Aug 10 20:53:43 2011 +0200
@@ -223,8 +223,8 @@
fun freeze_thaw_term t =
let
- val tvars = OldTerm.term_tvars t
- val tfree_names = OldTerm.add_term_tfree_names(t,[])
+ val tvars = Misc_Legacy.term_tvars t
+ val tfree_names = Misc_Legacy.add_term_tfree_names(t,[])
val (type_inst,_) =
fold (fn (w as (v,_), S) => fn (inst, used) =>
let
@@ -243,7 +243,7 @@
| inst_tfrees thy ((name,U)::rest) thm =
let
val cU = ctyp_of thy U
- val tfrees = OldTerm.add_term_tfrees (prop_of thm,[])
+ val tfrees = Misc_Legacy.add_term_tfrees (prop_of thm,[])
val (rens, thm') = Thm.varifyT_global'
(remove (op = o apsnd fst) name tfrees) thm
val mid =
@@ -494,7 +494,7 @@
let
val thy = Thm.theory_of_thm th
val c = prop_of th
- val vars = OldTerm.add_term_frees (c, OldTerm.add_term_vars(c,[]))
+ val vars = Misc_Legacy.add_term_frees (c, Misc_Legacy.add_term_vars(c,[]))
in
Drule.forall_intr_list (map (cterm_of thy) vars) th
end
@@ -560,7 +560,7 @@
fun set_prop thy t =
let
- val vars = OldTerm.add_term_frees (t, OldTerm.add_term_vars (t,[]))
+ val vars = Misc_Legacy.add_term_frees (t, Misc_Legacy.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/Matrix/Compute_Oracle/linker.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Wed Aug 10 20:53:43 2011 +0200
@@ -90,7 +90,7 @@
let
val cs = distinct_constants (filter is_polymorphic cs)
val old_cs = cs
-(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
+(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (Misc_Legacy.typ_tvars ty) tab
val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
fun tvars_of ty = collect_tvars ty Typtab.empty
val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
@@ -259,10 +259,10 @@
let
val (left, right) = collect_consts_of_thm th
val polycs = filter Linker.is_polymorphic left
- val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
+ val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (Misc_Legacy.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
fun check_const (c::cs) cs' =
let
- val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
+ val tvars = Misc_Legacy.typ_tvars (Linker.typ_of_constant c)
val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
in
if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
--- a/src/HOL/Matrix/matrixlp.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Matrix/matrixlp.ML Wed Aug 10 20:53:43 2011 +0200
@@ -19,7 +19,7 @@
fun inst_real thm =
let val certT = ctyp_of (Thm.theory_of_thm thm) in
Drule.export_without_context (Thm.instantiate
- ([(certT (TVar (hd (OldTerm.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
+ ([(certT (TVar (hd (Misc_Legacy.term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm)
end
local
@@ -57,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 (OldTerm.term_tvars (prop_of thm))))
+ val v = TVar (hd (sort ord (Misc_Legacy.term_tvars (prop_of thm))))
in
Drule.export_without_context (Thm.instantiate ([(certT v, certT ty)], []) thm)
end
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 10 20:53:43 2011 +0200
@@ -1414,7 +1414,7 @@
val _ = warning "defining recursion combinator ...";
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Aug 10 20:53:43 2011 +0200
@@ -69,7 +69,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)))
- (OldTerm.term_frees goal @ bvs);
+ (Misc_Legacy.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)
@@ -78,7 +78,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 (OldTerm.term_vars (prop_of exists_fresh'));
+ val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
in
(cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
rtac fs_name_thm 1 THEN
@@ -137,7 +137,7 @@
val fresh_perm_app = Global_Theory.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 (OldTerm.term_vars (prop_of exI)));
+ val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
val goal = nth (prems_of thm) (i-1);
val atom_name_opt = get_inner_fresh_fun goal;
val n = length (Logic.strip_params goal);
@@ -152,7 +152,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' = OldTerm.term_vars (prop_of st);
+ let val vars' = Misc_Legacy.term_vars (prop_of st);
val thy = theory_of_thm st;
in case subtract (op =) vars vars' of
[x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
@@ -161,7 +161,7 @@
in
((fn st =>
let
- val vars = OldTerm.term_vars (prop_of st);
+ val vars = Misc_Legacy.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_primrec.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Aug 10 20:53:43 2011 +0200
@@ -76,7 +76,7 @@
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
check_vars "extra variables on rhs: "
- (map dest_Free (OldTerm.term_frees rhs) |> subtract (op =) lfrees
+ (map dest_Free (Misc_Legacy.term_frees rhs) |> subtract (op =) lfrees
|> filter_out (is_fixed o fst));
case AList.lookup (op =) rec_fns fname of
NONE =>
--- a/src/HOL/Statespace/state_space.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Aug 10 20:53:43 2011 +0200
@@ -472,7 +472,7 @@
let
val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
val T = Syntax.read_typ ctxt' raw_T;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
fun cert_typ ctxt raw_T env =
@@ -480,7 +480,7 @@
val thy = Proof_Context.theory_of ctxt;
val T = Type.no_tvars (Sign.certify_typ thy raw_T)
handle TYPE (msg, _, _) => error msg;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
fun gen_define_statespace prep_typ state_space args name parents comps thy =
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Aug 10 20:53:43 2011 +0200
@@ -545,12 +545,12 @@
|> HOLogic.dest_eq
in
(Definition (name, t1, t2),
- fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
+ fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
end
| decode_line sym_tab (Inference (name, u, deps)) ctxt =
let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
(Inference (name, t, deps),
- fold Variable.declare_term (OldTerm.term_frees t) ctxt)
+ fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
end
fun decode_lines ctxt sym_tab lines =
fst (fold_map (decode_line sym_tab) lines ctxt)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 20:53:43 2011 +0200
@@ -1457,8 +1457,8 @@
#> List.foldl add_classes Symtab.empty
#> delete_type #> Symtab.keys
-val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
-val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
+val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
+val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
fun fold_type_constrs f (Type (s, Ts)) x =
fold (fold_type_constrs f) Ts (f (s, x))
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Aug 10 20:53:43 2011 +0200
@@ -77,7 +77,7 @@
else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs;
val arities = remove (op =) 0 (Datatype_Aux.get_arities descr');
val unneeded_vars =
- subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+ subtract (op =) (List.foldr Misc_Legacy.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val (newTs, oldTs) = chop (length (hd descr)) recTs;
@@ -372,7 +372,7 @@
val prop = Thm.prop_of thm;
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
- val used = OldTerm.add_term_tfree_names (a, []);
+ val used = Misc_Legacy.add_term_tfree_names (a, []);
fun mk_thm i =
let
@@ -676,7 +676,7 @@
let
val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
val _ =
- (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
+ (case subtract (op =) tvs (fold (curry Misc_Legacy.add_typ_tfree_names) cargs' []) of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs));
val c = Sign.full_name_path tmp_thy tname' cname;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Aug 10 20:53:43 2011 +0200
@@ -91,7 +91,7 @@
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = 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' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Aug 10 20:53:43 2011 +0200
@@ -144,7 +144,7 @@
fun abstr (t1, t2) =
(case t1 of
NONE =>
- (case flt (OldTerm.term_frees t2) of
+ (case flt (Misc_Legacy.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/datatype_case.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Aug 10 20:53:43 2011 +0200
@@ -318,7 +318,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 (OldTerm.add_term_names (u, used))
+ val xs' = map Free (Name.variant_list (Misc_Legacy.add_term_names (u, used))
(map fst xs) ~~ map snd xs)
in (xs', subst_bounds (rev xs', u)) end;
fun is_dependent i t =
@@ -379,9 +379,9 @@
fun strip_case'' dest (pat, rhs) =
(case dest (Term.add_free_names pat []) rhs of
SOME (exp as Free _, clauses) =>
- if member op aconv (OldTerm.term_frees pat) exp andalso
+ if member op aconv (Misc_Legacy.term_frees pat) exp andalso
not (exists (fn (_, rhs') =>
- member op aconv (OldTerm.term_frees rhs') exp) clauses)
+ member op aconv (Misc_Legacy.term_frees rhs') exp) clauses)
then
maps (strip_case'' dest) (map (fn (pat', rhs') =>
(subst_free [(exp, pat')] pat, rhs')) clauses)
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Aug 10 20:53:43 2011 +0200
@@ -331,8 +331,8 @@
let
val ts1 = take i ts;
val t :: ts2 = drop i ts;
- val names = List.foldr OldTerm.add_term_names
- (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
+ val names = List.foldr Misc_Legacy.add_term_names
+ (map (fst o fst o dest_Var) (List.foldr Misc_Legacy.add_term_vars [] ts1)) ts1;
val (Ts, dT) = split_last (take (i+1) (binder_types T));
fun pcase [] [] [] gr = ([], gr)
--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Aug 10 20:53:43 2011 +0200
@@ -398,7 +398,7 @@
Syntax.string_of_typ ctxt T);
fun type_of_constr (cT as (_, T)) =
let
- val frees = OldTerm.typ_tfrees T;
+ val frees = Misc_Legacy.typ_tfrees T;
val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
handle TYPE _ => no_constr cT
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Aug 10 20:53:43 2011 +0200
@@ -210,7 +210,7 @@
let
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
@@ -261,7 +261,7 @@
let
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
@@ -308,7 +308,7 @@
let
val descr' = flat descr;
val recTs = Datatype_Aux.get_rec_types descr' sorts;
- val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
+ val used' = List.foldr Misc_Legacy.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Aug 10 20:53:43 2011 +0200
@@ -65,7 +65,7 @@
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
- val args = OldTerm.term_frees body
+ val args = Misc_Legacy.term_frees body
(* Forms a lambda-abstraction over the formal parameters *)
val rhs =
list_abs_free (map dest_Free args,
@@ -75,7 +75,7 @@
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
(*Universal quant: insert a free variable into body and continue*)
- let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
+ let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
| dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
@@ -92,9 +92,9 @@
| is_quasi_lambda_free (Abs _) = false
| is_quasi_lambda_free _ = true
-val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
+val [f_B,g_B] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (Misc_Legacy.term_vars (prop_of @{thm abs_S}));
(* FIXME: Requires more use of cterm constructors. *)
fun abstract ct =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Aug 10 20:53:43 2011 +0200
@@ -372,7 +372,7 @@
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
val eq_terms = map (pairself (cterm_of thy))
- (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
+ (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
val factor = Seq.hd o distinct_subgoals_tac
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Aug 10 20:53:43 2011 +0200
@@ -560,7 +560,7 @@
fun conv ctxt p =
Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
- (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
+ (cons o term_of) (Misc_Legacy.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
(cooperex_conv ctxt) p
handle CTERM s => raise COOPER "bad cterm"
| THM s => raise COOPER "bad thm"
@@ -759,8 +759,8 @@
in
fun is_relevant ctxt ct =
subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
- andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
- andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
+ andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (Misc_Legacy.term_frees (term_of ct))
+ andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (Misc_Legacy.term_vars (term_of ct));
fun int_nat_terms ctxt ct =
let
--- a/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Wed Aug 10 20:53:43 2011 +0200
@@ -56,9 +56,9 @@
val abs_ct = ctermify abst;
val free_ct = ctermify x;
- val casethm_vars = rev (OldTerm.term_vars (Thm.concl_of case_thm));
+ val casethm_vars = rev (Misc_Legacy.term_vars (Thm.concl_of case_thm));
- val casethm_tvars = OldTerm.term_tvars (Thm.concl_of case_thm);
+ val casethm_tvars = Misc_Legacy.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 Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Wed Aug 10 20:53:43 2011 +0200
@@ -160,7 +160,7 @@
*---------------------------------------------------------------------------*)
local val thy = Thm.theory_of_thm disjI1
val prop = Thm.prop_of disjI1
- val [P,Q] = OldTerm.term_vars prop
+ val [P,Q] = Misc_Legacy.term_vars prop
val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
in
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
@@ -169,7 +169,7 @@
local val thy = Thm.theory_of_thm disjI2
val prop = Thm.prop_of disjI2
- val [P,Q] = OldTerm.term_vars prop
+ val [P,Q] = Misc_Legacy.term_vars prop
val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
in
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
@@ -263,7 +263,7 @@
local (* this is fragile *)
val thy = Thm.theory_of_thm spec
val prop = Thm.prop_of spec
- val x = hd (tl (OldTerm.term_vars prop))
+ val x = hd (tl (Misc_Legacy.term_vars prop))
val cTV = ctyp_of thy (type_of x)
val gspec = Thm.forall_intr (cterm_of thy x) spec
in
@@ -280,7 +280,7 @@
(* Not optimized! Too complicated. *)
local val thy = Thm.theory_of_thm allI
val prop = Thm.prop_of allI
- val [P] = OldTerm.add_term_vars (prop, [])
+ val [P] = Misc_Legacy.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
@@ -310,7 +310,7 @@
let val thy = Thm.theory_of_thm thm
val prop = Thm.prop_of thm
val tycheck = cterm_of thy
- val vlist = map tycheck (OldTerm.add_term_vars (prop, []))
+ val vlist = map tycheck (Misc_Legacy.add_term_vars (prop, []))
in GENL vlist thm
end;
@@ -350,7 +350,7 @@
local val thy = Thm.theory_of_thm exI
val prop = Thm.prop_of exI
- val [P,x] = OldTerm.term_vars prop
+ val [P,x] = Misc_Legacy.term_vars prop
in
fun EXISTS (template,witness) thm =
let val thy = Thm.theory_of_thm thm
@@ -501,7 +501,7 @@
val (f,args) = USyntax.strip_comb (get_lhs eq)
val (vstrl,_) = USyntax.strip_abs f
val names =
- Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
+ Name.variant_list (Misc_Legacy.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)
| Utils.ERR _ => get (rst, n+1, L);
@@ -742,7 +742,7 @@
val thy = Thm.theory_of_thm thm
val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
- (OldTerm.add_term_frees(tm,[]))
+ (Misc_Legacy.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
end
(*--------------------------------------------------------------
@@ -780,7 +780,7 @@
(if (is_cong thm) then cong_prover else restrict_prover) ss thm
end
val ctm = cprop_of th
- val names = OldTerm.add_term_names (term_of ctm, [])
+ val names = Misc_Legacy.add_term_names (term_of ctm, [])
val th1 = Raw_Simplifier.rewrite_cterm (false,true,false)
(prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
val th2 = Thm.equal_elim th1 th
--- a/src/HOL/Tools/TFL/tfl.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Aug 10 20:53:43 2011 +0200
@@ -322,7 +322,7 @@
val dummy = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
map_index (fn (i, t) => (t,(i,true))) R)
- val names = List.foldr OldTerm.add_term_names [] R
+ val names = List.foldr Misc_Legacy.add_term_names [] R
val atype = type_of(hd pats)
and aname = singleton (Name.variant_list names) "a"
val a = Free(aname,atype)
@@ -480,7 +480,7 @@
val tych = Thry.typecheck thy
val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
+ val R = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] eqns)) Rname,
Rtype)
val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
@@ -677,7 +677,7 @@
let val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
- let val names = List.foldr OldTerm.add_term_names [] pats
+ let val names = List.foldr Misc_Legacy.add_term_names [] pats
val T = type_of (hd pats)
val aname = singleton (Name.variant_list names) "a"
val vname = singleton (Name.variant_list (aname::names)) "v"
@@ -830,7 +830,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 = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
+ val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
[] (pats::TCsl))) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = Rules.SPEC (tych P) Sinduction
@@ -843,7 +843,7 @@
val proved_cases = map (prove_case fconst thy) tasks
val v =
Free (singleton
- (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
+ (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
domain)
val vtyped = tych v
val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
--- a/src/HOL/Tools/TFL/usyntax.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Wed Aug 10 20:53:43 2011 +0200
@@ -112,7 +112,7 @@
val is_vartype = can dest_vtype;
-val type_vars = map mk_prim_vartype o OldTerm.typ_tvars
+val type_vars = map mk_prim_vartype o Misc_Legacy.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 OldTerm.term_tvars;
+val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
@@ -319,7 +319,7 @@
(* Need to reverse? *)
-fun gen_all tm = list_mk_forall(OldTerm.term_frees tm, tm);
+fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
(* Destructing a cterm to a list of Terms *)
fun strip_comb tm =
--- a/src/HOL/Tools/choice_specification.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/choice_specification.ML Wed Aug 10 20:53:43 2011 +0200
@@ -18,7 +18,7 @@
fun close_form t =
fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
- (map dest_Free (OldTerm.term_frees t)) t
+ (map dest_Free (Misc_Legacy.term_frees t)) t
local
fun mk_definitional [] arg = arg
@@ -122,7 +122,7 @@
fun proc_single prop =
let
- val frees = OldTerm.term_frees prop
+ val frees = Misc_Legacy.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 = close_form prop
--- a/src/HOL/Tools/cnf_funcs.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Wed Aug 10 20:53:43 2011 +0200
@@ -511,7 +511,7 @@
NONE
in
Int.max (max, the_default 0 idx)
- end) (OldTerm.term_frees simp) 0)
+ end) (Misc_Legacy.term_frees simp) 0)
(* finally, convert to definitional CNF (this should preserve the simplification) *)
val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
(*###
--- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 10 20:53:43 2011 +0200
@@ -141,7 +141,7 @@
(fn (m, rnd) => string_of_mode m ^
(if rnd then " (random)" else "")) ms)) modes));
-val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
+val term_vs = map (fst o fst o dest_Var) o Misc_Legacy.term_vars;
val terms_vs = distinct (op =) o maps term_vs;
(** collect all Vars in a term (with duplicates!) **)
--- a/src/HOL/Tools/record.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/record.ML Wed Aug 10 20:53:43 2011 +0200
@@ -1512,7 +1512,7 @@
let
val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
val T = Syntax.read_typ ctxt' raw_T;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
fun cert_typ ctxt raw_T env =
@@ -1520,7 +1520,7 @@
val thy = Proof_Context.theory_of ctxt;
val T = Type.no_tvars (Sign.certify_typ thy raw_T)
handle TYPE (msg, _, _) => error msg;
- val env' = OldTerm.add_typ_tfrees (T, env);
+ val env' = Misc_Legacy.add_typ_tfrees (T, env);
in (T, env') end;
--- a/src/HOL/Tools/refute.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/refute.ML Wed Aug 10 20:53:43 2011 +0200
@@ -403,7 +403,7 @@
fun close_form t =
let
(* (Term.indexname * Term.typ) list *)
- val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
+ val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
in
fold (fn ((x, i), T) => fn t' =>
Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
@@ -1212,7 +1212,7 @@
(* existential closure over schematic variables *)
(* (Term.indexname * Term.typ) list *)
- val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
+ val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
(* Term.term *)
val ex_closure = fold (fn ((x, i), T) => fn t' =>
HOLogic.exists_const T $
--- a/src/HOL/Tools/split_rule.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/split_rule.ML Wed Aug 10 20:53:43 2011 +0200
@@ -88,7 +88,7 @@
(*curries ALL function variables occurring in a rule's conclusion*)
fun split_rule rl =
- fold_rev split_rule_var' (OldTerm.term_vars (concl_of rl)) rl
+ fold_rev split_rule_var' (Misc_Legacy.term_vars (concl_of rl)) rl
|> remove_internal_split
|> Drule.export_without_context;
--- a/src/Pure/IsaMakefile Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Pure/IsaMakefile Wed Aug 10 20:53:43 2011 +0200
@@ -232,7 +232,6 @@
morphism.ML \
name.ML \
net.ML \
- old_term.ML \
pattern.ML \
primitive_defs.ML \
proofterm.ML \
--- a/src/Pure/ROOT.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Pure/ROOT.ML Wed Aug 10 20:53:43 2011 +0200
@@ -119,7 +119,6 @@
use "term_ord.ML";
use "term_subst.ML";
use "term_xml.ML";
-use "old_term.ML";
use "General/name_space.ML";
use "sorts.ML";
use "type.ML";
--- a/src/Pure/old_term.ML Wed Aug 10 20:12:36 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-(* Title: Pure/old_term.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Some outdated term operations.
-*)
-
-signature OLD_TERM =
-sig
- val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
- 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 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
-end;
-
-structure OldTerm: OLD_TERM =
-struct
-
-(*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 in the term, suppressing duplicates.
- Includes Frees and Consts. For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name 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;
-
-(*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,[]);
-
-
-(*Accumulates the Vars in the term, suppressing duplicates.*)
-fun add_term_vars (t, vars: term list) = case t of
- Var _ => Ord_List.insert Term_Ord.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 _ => Ord_List.insert Term_Ord.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,[]);
-
-end;
--- a/src/Tools/Code_Generator.thy Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Tools/Code_Generator.thy Wed Aug 10 20:53:43 2011 +0200
@@ -7,6 +7,7 @@
theory Code_Generator
imports Pure
uses
+ "~~/src/Tools/misc_legacy.ML"
"~~/src/Tools/codegen.ML"
"~~/src/Tools/cache_io.ML"
"~~/src/Tools/try.ML"
--- a/src/Tools/IsaPlanner/isand.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Wed Aug 10 20:53:43 2011 +0200
@@ -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 OldTerm.add_term_tfrees [] ts);
- val tvars = List.foldr OldTerm.add_term_tvars [] ts;
+ val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
+ val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
val (names',renamings) =
List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
let val n2 = singleton (Name.variant_list Ns) n in
@@ -212,15 +212,15 @@
fun unfix_tfrees ns th =
let
val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
- val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
+ val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
in #2 (Thm.varifyT_global' skiptfrees th) end;
(* change schematic/meta vars to fresh free vars, avoiding name clashes
with "names" *)
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 OldTerm.add_term_names names ts;
+ val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
+ val Ns = List.foldr Misc_Legacy.add_term_names names ts;
val (_,renamings) =
Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
let val n2 = singleton (Name.variant_list 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 OldTerm.add_term_tvars [] (prop :: tpairs);
+ val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
val ctyfixes =
map_filter
(fn (v as ((s,i),ty)) =>
@@ -258,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 OldTerm.add_term_vars
+ val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars
[] (prop :: tpairs));
val cfixes =
map_filter
@@ -359,7 +359,7 @@
val sgn = Thm.theory_of_thm th;
val ctermify = Thm.cterm_of sgn;
- val allfrees = map Term.dest_Free (OldTerm.term_frees (Thm.prop_of th))
+ val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
val cfrees = map (ctermify o Free o lookupfree allfrees) vs
val sgs = prems_of th;
@@ -419,8 +419,8 @@
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) (OldTerm.term_vars t)
- val names = OldTerm.add_term_names (t,varnames);
+ val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
+ val names = Misc_Legacy.add_term_names (t,varnames);
val fvs = map Free
(Name.variant_list names (map fst alls)
~~ (map snd alls));
@@ -428,8 +428,8 @@
fun fix_alls_term i t =
let
- val varnames = map (fst o fst o Term.dest_Var) (OldTerm.term_vars t)
- val names = OldTerm.add_term_names (t,varnames);
+ val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
+ val names = Misc_Legacy.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 Aug 10 20:12:36 2011 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Aug 10 20:53:43 2011 +0200
@@ -71,7 +71,7 @@
val (tpairl,tpairr) = Library.split_list (#tpairs rep)
val prop = #prop rep
in
- List.foldr OldTerm.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
+ List.foldr Misc_Legacy.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
end;
(* Given a list of variables that were bound, and a that has been
@@ -136,13 +136,13 @@
fun mk_renamings tgt rule_inst =
let
val rule_conds = Thm.prems_of rule_inst
- val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
+ val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
val (conds_tyvs,cond_vs) =
Library.foldl (fn ((tyvs, vs), t) =>
- (union (op =) (OldTerm.term_tvars t) tyvs,
- union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs))
+ (union (op =) (Misc_Legacy.term_tvars t) tyvs,
+ union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
(([],[]), rule_conds);
- val termvars = map Term.dest_Var (OldTerm.term_vars tgt);
+ val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
val vars_to_fix = union (op =) termvars cond_vs;
val (renamings, names2) =
List.foldr (fn (((n,i),ty), (vs, names')) =>
@@ -165,8 +165,8 @@
val ignore_ixs = map fst ignore_insts;
val (tvars, tfrees) =
List.foldr (fn (t, (varixs, tfrees)) =>
- (OldTerm.add_term_tvars (t,varixs),
- OldTerm.add_term_tfrees (t,tfrees)))
+ (Misc_Legacy.add_term_tvars (t,varixs),
+ Misc_Legacy.add_term_tfrees (t,tfrees)))
([],[]) ts;
val unfixed_tvars =
filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
--- a/src/Tools/codegen.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Tools/codegen.ML Wed Aug 10 20:53:43 2011 +0200
@@ -273,7 +273,7 @@
fun preprocess_term thy t =
let
- val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
+ val x = Free (singleton (Name.variant_list (Misc_Legacy.add_term_names (t, []))) "x", fastype_of t);
(* fake definition *)
val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
fun err () = error "preprocess_term: bad preprocessor"
@@ -446,7 +446,7 @@
fun rename_terms ts =
let
- val names = List.foldr OldTerm.add_term_names
+ val names = List.foldr Misc_Legacy.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 =>
@@ -471,7 +471,7 @@
(**** retrieve definition of constant ****)
fun is_instance T1 T2 =
- Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
+ Type.raw_instance (T1, if null (Misc_Legacy.typ_tfrees T2) then T2 else Logic.varifyT_global 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)));
@@ -592,8 +592,8 @@
else Pretty.block (separate (Pretty.brk 1) (p :: ps));
fun new_names t xs = Name.variant_list
- (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t))
- (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
+ (union (op =) (map (fst o fst o dest_Var) (Misc_Legacy.term_vars t))
+ (Misc_Legacy.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
fun new_name t x = hd (new_names t [x]);
--- a/src/Tools/misc_legacy.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/Tools/misc_legacy.ML Wed Aug 10 20:53:43 2011 +0200
@@ -5,6 +5,22 @@
signature MISC_LEGACY =
sig
+ val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
+ 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 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 mk_defpair: term * term -> string * term
val get_def: theory -> xstring -> thm
val simple_read_term: theory -> typ -> string -> term
@@ -14,6 +30,71 @@
structure Misc_Legacy: MISC_LEGACY =
struct
+(*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 in the term, suppressing duplicates.
+ Includes Frees and Consts. For choosing unambiguous bound var names.*)
+fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name 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;
+
+(*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,[]);
+
+
+(*Accumulates the Vars in the term, suppressing duplicates.*)
+fun add_term_vars (t, vars: term list) = case t of
+ Var _ => Ord_List.insert Term_Ord.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 _ => Ord_List.insert Term_Ord.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,[]);
+
+
fun mk_defpair (lhs, rhs) =
(case Term.head_of lhs of
Const (name, _) =>
--- a/src/ZF/Tools/inductive_package.ML Wed Aug 10 20:12:36 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Aug 10 20:53:43 2011 +0200
@@ -96,7 +96,7 @@
Syntax.string_of_term ctxt t);
(*** Construct the fixedpoint definition ***)
- val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
+ val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
@@ -108,7 +108,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 (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
- val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
+ val exfrees = subtract (op =) rec_params (Misc_Legacy.term_frees intr)
val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
in List.foldr FOLogic.mk_exists
(Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
@@ -296,7 +296,7 @@
(*Make a premise of the induction rule.*)
fun induct_prem ind_alist intr =
- let val quantfrees = map dest_Free (subtract (op =) rec_params (OldTerm.term_frees intr))
+ let val quantfrees = map dest_Free (subtract (op =) rec_params (Misc_Legacy.term_frees intr))
val iprems = List.foldr (add_induct_prem ind_alist) []
(Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr