# HG changeset patch # User wenzelm # Date 1313002423 -7200 # Node ID 44adaa6db327d501c70c035b0af90f94f48e3863 # Parent 01de796250a071b2d738275a618df4afc6b4104f old term operations are legacy; diff -r 01de796250a0 -r 44adaa6db327 src/FOL/IFOL.thy --- 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" diff -r 01de796250a0 -r 44adaa6db327 src/FOL/IsaMakefile --- 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 \ diff -r 01de796250a0 -r 44adaa6db327 src/FOLP/IFOLP.thy --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/FOLP/IsaMakefile --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/FOLP/simp.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/Cooper.thy --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/MIR.thy --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/commutative_ring_tac.ML --- 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); diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/cooper_tac.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/ferrack_tac.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/langford.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Decision_Procs/mir_tac.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/HOL.thy --- 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" diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Import/proof_kernel.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) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Import/shuffler.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Matrix/Compute_Oracle/linker.ML --- 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" diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Matrix/matrixlp.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Nominal/nominal_datatype.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Nominal/nominal_fresh_fun.ML --- 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. *) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Nominal/nominal_primrec.ML --- 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 => diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Statespace/state_space.ML --- 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 = diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/ATP/atp_translate.ML --- 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)) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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); diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_aux.ML --- 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)))) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_case.ML --- 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) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_codegen.ML --- 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) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_data.ML --- 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 (); diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_prop.ML --- 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); diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Meson/meson_clausify.ML --- 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 = diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/TFL/casesplit.ML --- 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)))) => diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/TFL/rules.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/TFL/tfl.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/TFL/usyntax.ML --- 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 = diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/choice_specification.ML --- 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 diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/cnf_funcs.ML --- 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 (*### diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/inductive_codegen.ML --- 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!) **) diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/record.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/refute.ML --- 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 $ diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/split_rule.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/Pure/IsaMakefile --- 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 \ diff -r 01de796250a0 -r 44adaa6db327 src/Pure/ROOT.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"; diff -r 01de796250a0 -r 44adaa6db327 src/Pure/old_term.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; diff -r 01de796250a0 -r 44adaa6db327 src/Tools/Code_Generator.thy --- 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" diff -r 01de796250a0 -r 44adaa6db327 src/Tools/IsaPlanner/isand.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); diff -r 01de796250a0 -r 44adaa6db327 src/Tools/IsaPlanner/rw_inst.ML --- 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; diff -r 01de796250a0 -r 44adaa6db327 src/Tools/codegen.ML --- 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]); diff -r 01de796250a0 -r 44adaa6db327 src/Tools/misc_legacy.ML --- 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, _) => diff -r 01de796250a0 -r 44adaa6db327 src/ZF/Tools/inductive_package.ML --- 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