more explicit context;
authorwenzelm
Tue Jul 28 20:59:39 2015 +0200 (2015-07-28)
changeset 608224f58f3662e7d
parent 60821 f7f4d5f7920e
child 60823 b41478500473
more explicit context;
src/FOL/simpdata.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/simpdata.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/object_logic.ML
src/Pure/drule.ML
src/Pure/raw_simplifier.ML
src/Pure/variable.ML
src/Sequents/simpdata.ML
src/ZF/Main_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/Tools/inductive_package.ML
src/ZF/pair.thy
     1.1 --- a/src/FOL/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Jul 28 20:59:39 2015 +0200
     1.3 @@ -50,8 +50,7 @@
     1.4         | _ => [th])
     1.5    in atoms end;
     1.6  
     1.7 -fun mksimps pairs ctxt =
     1.8 -  map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
     1.9 +fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt;
    1.10  
    1.11  
    1.12  (** make simplification procedures for quantifier elimination **)
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jul 28 20:15:19 2015 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Jul 28 20:59:39 2015 +0200
     2.3 @@ -800,7 +800,7 @@
     2.4  
     2.5                fun make_sel_thm xs' case_thm sel_def =
     2.6                  zero_var_indexes
     2.7 -                  (Drule.gen_all (Variable.maxidx_of lthy)
     2.8 +                  (Variable.gen_all lthy
     2.9                      (Drule.rename_bvars'
    2.10                        (map (SOME o fst) xs')
    2.11                        (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
     3.1 --- a/src/HOL/Tools/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
     3.2 +++ b/src/HOL/Tools/simpdata.ML	Tue Jul 28 20:59:39 2015 +0200
     3.3 @@ -112,8 +112,7 @@
     3.4        end;
     3.5    in atoms end;
     3.6  
     3.7 -fun mksimps pairs ctxt =
     3.8 -  map_filter (try mk_eq) o mk_atomize ctxt pairs o Drule.gen_all (Variable.maxidx_of ctxt);
     3.9 +fun mksimps pairs ctxt = map_filter (try mk_eq) o mk_atomize ctxt pairs o Variable.gen_all ctxt;
    3.10  
    3.11  fun unsafe_solver_tac ctxt =
    3.12    let
     4.1 --- a/src/Pure/Isar/local_defs.ML	Tue Jul 28 20:15:19 2015 +0200
     4.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Jul 28 20:59:39 2015 +0200
     4.3 @@ -131,6 +131,8 @@
     4.4  *)
     4.5  fun export inner outer =    (*beware of closure sizes*)
     4.6    let
     4.7 +    val thy = Proof_Context.theory_of inner;
     4.8 +    val maxidx0 = Variable.maxidx_of outer;
     4.9      val exp = Assumption.export false inner outer;
    4.10      val exp_term = Assumption.export_term inner outer;
    4.11      val asms = Assumption.local_assms_of inner outer;
    4.12 @@ -149,7 +151,7 @@
    4.13                      NONE => (asm, false)
    4.14                    | SOME u =>
    4.15                        if t aconv u then (asm, false)
    4.16 -                      else (Drule.abs_def (Drule.gen_all (Variable.maxidx_of outer) asm), true))
    4.17 +                      else (Drule.abs_def (Drule.gen_all thy maxidx0 asm), true))
    4.18                  end)));
    4.19        in (apply2 (map #1) (List.partition #2 defs_asms), th') end
    4.20    end;
     5.1 --- a/src/Pure/Isar/object_logic.ML	Tue Jul 28 20:15:19 2015 +0200
     5.2 +++ b/src/Pure/Isar/object_logic.ML	Tue Jul 28 20:59:39 2015 +0200
     5.3 @@ -203,7 +203,7 @@
     5.4  
     5.5  fun gen_rulify full ctxt =
     5.6    Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
     5.7 -  #> Drule.gen_all (Variable.maxidx_of ctxt)
     5.8 +  #> Variable.gen_all ctxt
     5.9    #> Thm.strip_shyps
    5.10    #> Drule.zero_var_indexes;
    5.11  
     6.1 --- a/src/Pure/drule.ML	Tue Jul 28 20:15:19 2015 +0200
     6.2 +++ b/src/Pure/drule.ML	Tue Jul 28 20:59:39 2015 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4    val forall_intr_list: cterm list -> thm -> thm
     6.5    val forall_intr_vars: thm -> thm
     6.6    val forall_elim_list: cterm list -> thm -> thm
     6.7 -  val gen_all: int -> thm -> thm
     6.8 +  val gen_all: theory -> int -> thm -> thm
     6.9    val lift_all: Proof.context -> cterm -> thm -> thm
    6.10    val implies_elim_list: thm -> thm list -> thm
    6.11    val implies_intr_list: cterm list -> thm -> thm
    6.12 @@ -183,9 +183,8 @@
    6.13    in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
    6.14  
    6.15  (*generalize outermost parameters*)
    6.16 -fun gen_all maxidx0 th =
    6.17 +fun gen_all thy maxidx0 th =
    6.18    let
    6.19 -    val thy = Thm.theory_of_thm th;
    6.20      val maxidx = Thm.maxidx_thm th maxidx0;
    6.21      val prop = Thm.prop_of th;
    6.22      fun elim (x, T) =
     7.1 --- a/src/Pure/raw_simplifier.ML	Tue Jul 28 20:15:19 2015 +0200
     7.2 +++ b/src/Pure/raw_simplifier.ML	Tue Jul 28 20:59:39 2015 +0200
     7.3 @@ -1385,7 +1385,7 @@
     7.4      Conv.fconv_rule
     7.5        (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
     7.6    |> Thm.adjust_maxidx_thm ~1
     7.7 -  |> Drule.gen_all (Variable.maxidx_of ctxt);
     7.8 +  |> Variable.gen_all ctxt;
     7.9  
    7.10  val hhf_ss =
    7.11    simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))
     8.1 --- a/src/Pure/variable.ML	Tue Jul 28 20:15:19 2015 +0200
     8.2 +++ b/src/Pure/variable.ML	Tue Jul 28 20:59:39 2015 +0200
     8.3 @@ -59,6 +59,7 @@
     8.4    val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
     8.5    val variant_fixes: string list -> Proof.context -> string list * Proof.context
     8.6    val dest_fixes: Proof.context -> (string * string) list
     8.7 +  val gen_all: Proof.context -> thm -> thm
     8.8    val export_terms: Proof.context -> Proof.context -> term list -> term list
     8.9    val exportT_terms: Proof.context -> Proof.context -> term list -> term list
    8.10    val exportT: Proof.context -> Proof.context -> thm list -> thm list
    8.11 @@ -497,6 +498,8 @@
    8.12  
    8.13  (** export -- generalize type/term variables (beware of closure sizes) **)
    8.14  
    8.15 +fun gen_all ctxt = Drule.gen_all (Proof_Context.theory_of ctxt) (maxidx_of ctxt);
    8.16 +
    8.17  fun export_inst inner outer =
    8.18    let
    8.19      val declared_outer = is_declared outer;
     9.1 --- a/src/Sequents/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
     9.2 +++ b/src/Sequents/simpdata.ML	Tue Jul 28 20:59:39 2015 +0200
     9.3 @@ -71,8 +71,7 @@
     9.4    setSSolver (mk_solver "safe" safe_solver)
     9.5    setSolver (mk_solver "unsafe" unsafe_solver)
     9.6    |> Simplifier.set_subgoaler asm_simp_tac
     9.7 -  |> Simplifier.set_mksimps (fn ctxt =>
     9.8 -      map (mk_meta_eq ctxt) o atomize o Drule.gen_all (Variable.maxidx_of ctxt))
     9.9 +  |> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt)
    9.10    |> Simplifier.set_mkcong mk_meta_cong
    9.11    |> simpset_of;
    9.12  
    10.1 --- a/src/ZF/Main_ZF.thy	Tue Jul 28 20:15:19 2015 +0200
    10.2 +++ b/src/ZF/Main_ZF.thy	Tue Jul 28 20:59:39 2015 +0200
    10.3 @@ -72,7 +72,7 @@
    10.4  
    10.5  declaration \<open>fn _ =>
    10.6    Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    10.7 -    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
    10.8 +    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
    10.9  \<close>
   10.10  
   10.11  end
    11.1 --- a/src/ZF/OrdQuant.thy	Tue Jul 28 20:15:19 2015 +0200
    11.2 +++ b/src/ZF/OrdQuant.thy	Tue Jul 28 20:59:39 2015 +0200
    11.3 @@ -362,7 +362,7 @@
    11.4  \<close>
    11.5  declaration \<open>fn _ =>
    11.6    Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
    11.7 -    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
    11.8 +    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
    11.9  \<close>
   11.10  
   11.11  text \<open>Setting up the one-point-rule simproc\<close>
    12.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jul 28 20:15:19 2015 +0200
    12.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 28 20:59:39 2015 +0200
    12.3 @@ -327,8 +327,7 @@
    12.4         If the premises get simplified, then the proofs could fail.*)
    12.5       val min_ss =
    12.6             (empty_simpset (Proof_Context.init_global thy)
    12.7 -             |> Simplifier.set_mksimps (fn ctxt =>
    12.8 -                 map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
    12.9 +             |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
   12.10             setSolver (mk_solver "minimal"
   12.11                        (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
   12.12                                     ORELSE' assume_tac ctxt
    13.1 --- a/src/ZF/pair.thy	Tue Jul 28 20:15:19 2015 +0200
    13.2 +++ b/src/ZF/pair.thy	Tue Jul 28 20:59:39 2015 +0200
    13.3 @@ -12,8 +12,7 @@
    13.4  
    13.5  setup \<open>
    13.6    map_theory_simpset
    13.7 -    (Simplifier.set_mksimps (fn ctxt =>
    13.8 -        map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))
    13.9 +    (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
   13.10        #> Simplifier.add_cong @{thm if_weak_cong})
   13.11  \<close>
   13.12