clarified context;
authorwenzelm
Wed Jul 08 21:33:00 2015 +0200 (2015-07-08)
changeset 606968304fb4fb823
parent 60695 757549b4bbe6
child 60697 e266d5463e9d
clarified context;
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/cnf.ML
src/HOL/Tools/reification.ML
src/HOL/Tools/set_comprehension_pointfree.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -709,7 +709,7 @@
     1.4              resolve_tac ctxt @{thms ccontr} 1,
     1.5              preskolem_tac,
     1.6              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
     1.7 -                      EVERY1 [skolemize_prems_tac ctxt negs,
     1.8 +                      EVERY1 [skolemize_prems_tac ctxt' negs,
     1.9                                Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
    1.10    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
    1.11  
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jul 08 19:28:43 2015 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Jul 08 21:33:00 2015 +0200
     2.3 @@ -947,7 +947,7 @@
     2.4      val U = TFree ("'u", @{sort type})
     2.5      val y = Free (yname, U)
     2.6      val f' = absdummy (U --> T') (Bound 0 $ y)
     2.7 -    val th' = Thm.certify_instantiate ctxt
     2.8 +    val th' = Thm.certify_instantiate ctxt'
     2.9        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    2.10         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    2.11      val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Jul 08 19:28:43 2015 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Jul 08 21:33:00 2015 +0200
     3.3 @@ -145,20 +145,20 @@
     3.4      THEN trace_tac ctxt options "after prove_match:"
     3.5      THEN (DETERM (TRY
     3.6             (rtac eval_if_P 1
     3.7 -           THEN (SUBPROOF (fn {prems, ...} =>
     3.8 +           THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
     3.9               (REPEAT_DETERM (rtac @{thm conjI} 1
    3.10 -             THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1))))
    3.11 -             THEN trace_tac ctxt options "if condition to be solved:"
    3.12 -             THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
    3.13 +             THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
    3.14 +             THEN trace_tac ctxt' options "if condition to be solved:"
    3.15 +             THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
    3.16               THEN TRY (
    3.17                  let
    3.18                    val prems' = maps dest_conjunct_prem (take nargs prems)
    3.19                  in
    3.20 -                  rewrite_goal_tac ctxt
    3.21 +                  rewrite_goal_tac ctxt'
    3.22                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    3.23                  end
    3.24               THEN REPEAT_DETERM (rtac @{thm refl} 1))
    3.25 -             THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1))))
    3.26 +             THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
    3.27      THEN trace_tac ctxt options "after if simplification"
    3.28    end;
    3.29  
     4.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 21:33:00 2015 +0200
     4.3 @@ -295,7 +295,7 @@
     4.4    fun tac prove ctxt rules =
     4.5      CONVERSION (SMT_Normalize.atomize_conv ctxt)
     4.6      THEN' rtac @{thm ccontr}
     4.7 -    THEN' SUBPROOF (fn {context = ctxt, prems, ...} => resolve (prove ctxt (rules @ prems))) ctxt
     4.8 +    THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve (prove ctxt' (rules @ prems))) ctxt
     4.9  in
    4.10  
    4.11  val smt_tac = tac safe_solve
     5.1 --- a/src/HOL/Tools/cnf.ML	Wed Jul 08 19:28:43 2015 +0200
     5.2 +++ b/src/HOL/Tools/cnf.ML	Wed Jul 08 21:33:00 2015 +0200
     5.3 @@ -539,9 +539,9 @@
     5.4  
     5.5  fun cnf_rewrite_tac ctxt i =
     5.6    (* cut the CNF formulas as new premises *)
     5.7 -  Subgoal.FOCUS (fn {prems, ...} =>
     5.8 +  Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
     5.9      let
    5.10 -      val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
    5.11 +      val cnf_thms = map (make_cnf_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems
    5.12        val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
    5.13      in
    5.14        cut_facts_tac cut_thms 1
    5.15 @@ -561,9 +561,9 @@
    5.16  
    5.17  fun cnfx_rewrite_tac ctxt i =
    5.18    (* cut the CNF formulas as new premises *)
    5.19 -  Subgoal.FOCUS (fn {prems, ...} =>
    5.20 +  Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
    5.21      let
    5.22 -      val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
    5.23 +      val cnfx_thms = map (make_cnfx_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems
    5.24        val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
    5.25      in
    5.26        cut_facts_tac cut_thms 1
     6.1 --- a/src/HOL/Tools/reification.ML	Wed Jul 08 19:28:43 2015 +0200
     6.2 +++ b/src/HOL/Tools/reification.ML	Wed Jul 08 21:33:00 2015 +0200
     6.3 @@ -23,11 +23,12 @@
     6.4  
     6.5  val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp}
     6.6  
     6.7 -fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn { concl, ... } =>
     6.8 +fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn {context = ctxt', concl, ...} =>
     6.9    let
    6.10 -    val ct = case some_t
    6.11 -     of NONE => Thm.dest_arg concl
    6.12 -      | SOME t => Thm.cterm_of ctxt t
    6.13 +    val ct =
    6.14 +      (case some_t of
    6.15 +        NONE => Thm.dest_arg concl
    6.16 +      | SOME t => Thm.cterm_of ctxt' t)
    6.17      val thm = conv ct;
    6.18    in
    6.19      if Thm.is_reflexive thm then no_tac
     7.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Jul 08 19:28:43 2015 +0200
     7.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Jul 08 21:33:00 2015 +0200
     7.3 @@ -441,9 +441,8 @@
     7.4        THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms exE}
     7.5        THEN' eresolve_tac ctxt @{thms conjE}
     7.6        THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
     7.7 -      THEN' Subgoal.FOCUS (fn {prems, ...} =>
     7.8 -        (* FIXME inner context!? *)
     7.9 -        simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
    7.10 +      THEN' Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
    7.11 +        simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (filter is_eq prems)) 1) ctxt
    7.12        THEN' TRY o assume_tac ctxt
    7.13    in
    7.14      case try mk_term (Thm.term_of ct) of