# HG changeset patch # User wenzelm # Date 1438109979 -7200 # Node ID 4f58f3662e7d6b7175303c5586269914092f6198 # Parent f7f4d5f7920e20f8adcbd1d7948b8de7dfa4ac5b more explicit context; diff -r f7f4d5f7920e -r 4f58f3662e7d src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/FOL/simpdata.ML Tue Jul 28 20:59:39 2015 +0200 @@ -50,8 +50,7 @@ | _ => [th]) in atoms end; -fun mksimps pairs ctxt = - map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt); +fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt; (** make simplification procedures for quantifier elimination **) diff -r f7f4d5f7920e -r 4f58f3662e7d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Jul 28 20:59:39 2015 +0200 @@ -800,7 +800,7 @@ fun make_sel_thm xs' case_thm sel_def = zero_var_indexes - (Drule.gen_all (Variable.maxidx_of lthy) + (Variable.gen_all lthy (Drule.rename_bvars' (map (SOME o fst) xs') (Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); diff -r f7f4d5f7920e -r 4f58f3662e7d src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/HOL/Tools/simpdata.ML Tue Jul 28 20:59:39 2015 +0200 @@ -112,8 +112,7 @@ end; in atoms end; -fun mksimps pairs ctxt = - map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt); +fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt; fun unsafe_solver_tac ctxt = let diff -r f7f4d5f7920e -r 4f58f3662e7d src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/Pure/Isar/local_defs.ML Tue Jul 28 20:59:39 2015 +0200 @@ -131,6 +131,8 @@ *) fun export inner outer = (*beware of closure sizes*) let + val thy = Proof_Context.theory_of inner; + val maxidx0 = Variable.maxidx_of outer; val exp = Assumption.export false inner outer; val exp_term = Assumption.export_term inner outer; val asms = Assumption.local_assms_of inner outer; @@ -149,7 +151,7 @@ NONE => (asm, false) | SOME u => if t aconv u then (asm, false) - else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true)) + else (Drule.abs_def (Drule.gen_all thy maxidx0 asm), true)) end))); in (apply2 (map #1) (List.partition #2 defs_asms), th') end end; diff -r f7f4d5f7920e -r 4f58f3662e7d src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/Pure/Isar/object_logic.ML Tue Jul 28 20:59:39 2015 +0200 @@ -203,7 +203,7 @@ fun gen_rulify full ctxt = Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt)) - #> Drule.gen_all (Variable.maxidx_of ctxt) + #> Variable.gen_all ctxt #> Thm.strip_shyps #> Drule.zero_var_indexes; diff -r f7f4d5f7920e -r 4f58f3662e7d src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/Pure/drule.ML Tue Jul 28 20:59:39 2015 +0200 @@ -16,7 +16,7 @@ val forall_intr_list: cterm list -> thm -> thm val forall_intr_vars: thm -> thm val forall_elim_list: cterm list -> thm -> thm - val gen_all: int -> thm -> thm + val gen_all: theory -> int -> thm -> thm val lift_all: Proof.context -> cterm -> thm -> thm val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm @@ -183,9 +183,8 @@ in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end; (*generalize outermost parameters*) -fun gen_all maxidx0 th = +fun gen_all thy maxidx0 th = let - val thy = Thm.theory_of_thm th; val maxidx = Thm.maxidx_thm th maxidx0; val prop = Thm.prop_of th; fun elim (x, T) = diff -r f7f4d5f7920e -r 4f58f3662e7d src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/Pure/raw_simplifier.ML Tue Jul 28 20:59:39 2015 +0200 @@ -1385,7 +1385,7 @@ Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th) |> Thm.adjust_maxidx_thm ~1 - |> Drule.gen_all (Variable.maxidx_of ctxt); + |> Variable.gen_all ctxt; val hhf_ss = simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ())) diff -r f7f4d5f7920e -r 4f58f3662e7d src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/Pure/variable.ML Tue Jul 28 20:59:39 2015 +0200 @@ -59,6 +59,7 @@ val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context val dest_fixes: Proof.context -> (string * string) list + val gen_all: Proof.context -> thm -> thm val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list val exportT: Proof.context -> Proof.context -> thm list -> thm list @@ -497,6 +498,8 @@ (** export -- generalize type/term variables (beware of closure sizes) **) +fun gen_all ctxt = Drule.gen_all (Proof_Context.theory_of ctxt) (maxidx_of ctxt); + fun export_inst inner outer = let val declared_outer = is_declared outer; diff -r f7f4d5f7920e -r 4f58f3662e7d src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/Sequents/simpdata.ML Tue Jul 28 20:59:39 2015 +0200 @@ -71,8 +71,7 @@ setSSolver (mk_solver "safe" safe_solver) setSolver (mk_solver "unsafe" unsafe_solver) |> Simplifier.set_subgoaler asm_simp_tac - |> Simplifier.set_mksimps (fn ctxt => - map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt)) + |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt) |> Simplifier.set_mkcong mk_meta_cong |> simpset_of; diff -r f7f4d5f7920e -r 4f58f3662e7d src/ZF/Main_ZF.thy --- a/src/ZF/Main_ZF.thy Tue Jul 28 20:15:19 2015 +0200 +++ b/src/ZF/Main_ZF.thy Tue Jul 28 20:59:39 2015 +0200 @@ -72,7 +72,7 @@ declaration \fn _ => Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => - map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) + map mk_eq o Ord_atomize o Variable.gen_all ctxt)) \ end diff -r f7f4d5f7920e -r 4f58f3662e7d src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Tue Jul 28 20:15:19 2015 +0200 +++ b/src/ZF/OrdQuant.thy Tue Jul 28 20:59:39 2015 +0200 @@ -362,7 +362,7 @@ \ declaration \fn _ => Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => - map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) + map mk_eq o Ord_atomize o Variable.gen_all ctxt)) \ text \Setting up the one-point-rule simproc\ diff -r f7f4d5f7920e -r 4f58f3662e7d src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Jul 28 20:15:19 2015 +0200 +++ b/src/ZF/Tools/inductive_package.ML Tue Jul 28 20:59:39 2015 +0200 @@ -327,8 +327,7 @@ If the premises get simplified, then the proofs could fail.*) val min_ss = (empty_simpset (Proof_Context.init_global thy) - |> Simplifier.set_mksimps (fn ctxt => - map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) + |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)) setSolver (mk_solver "minimal" (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) ORELSE' assume_tac ctxt diff -r f7f4d5f7920e -r 4f58f3662e7d src/ZF/pair.thy --- a/src/ZF/pair.thy Tue Jul 28 20:15:19 2015 +0200 +++ b/src/ZF/pair.thy Tue Jul 28 20:59:39 2015 +0200 @@ -12,8 +12,7 @@ setup \ map_theory_simpset - (Simplifier.set_mksimps (fn ctxt => - map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)) + (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt) #> Simplifier.add_cong @{thm if_weak_cong}) \