--- a/src/HOL/Tools/Meson/meson.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Wed Jul 08 21:33:00 2015 +0200
@@ -709,7 +709,7 @@
resolve_tac ctxt @{thms ccontr} 1,
preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [skolemize_prems_tac ctxt negs,
+ EVERY1 [skolemize_prems_tac ctxt' negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Jul 08 21:33:00 2015 +0200
@@ -947,7 +947,7 @@
val U = TFree ("'u", @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
- val th' = Thm.certify_instantiate ctxt
+ val th' = Thm.certify_instantiate ctxt'
([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
[((fst (dest_Var f), (U --> T') --> T'), f')]) th
val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Jul 08 21:33:00 2015 +0200
@@ -145,20 +145,20 @@
THEN trace_tac ctxt options "after prove_match:"
THEN (DETERM (TRY
(rtac eval_if_P 1
- THEN (SUBPROOF (fn {prems, ...} =>
+ THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
(REPEAT_DETERM (rtac @{thm conjI} 1
- THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1))))
- THEN trace_tac ctxt options "if condition to be solved:"
- THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
+ THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
+ THEN trace_tac ctxt' options "if condition to be solved:"
+ THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
THEN TRY (
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- rewrite_goal_tac ctxt
+ rewrite_goal_tac ctxt'
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end
THEN REPEAT_DETERM (rtac @{thm refl} 1))
- THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1))))
+ THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
THEN trace_tac ctxt options "after if simplification"
end;
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Jul 08 21:33:00 2015 +0200
@@ -295,7 +295,7 @@
fun tac prove ctxt rules =
CONVERSION (SMT_Normalize.atomize_conv ctxt)
THEN' rtac @{thm ccontr}
- THEN' SUBPROOF (fn {context = ctxt, prems, ...} => resolve (prove ctxt (rules @ prems))) ctxt
+ THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve (prove ctxt' (rules @ prems))) ctxt
in
val smt_tac = tac safe_solve
--- a/src/HOL/Tools/cnf.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/cnf.ML Wed Jul 08 21:33:00 2015 +0200
@@ -539,9 +539,9 @@
fun cnf_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- Subgoal.FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
let
- val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
+ val cnf_thms = map (make_cnf_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
in
cut_facts_tac cut_thms 1
@@ -561,9 +561,9 @@
fun cnfx_rewrite_tac ctxt i =
(* cut the CNF formulas as new premises *)
- Subgoal.FOCUS (fn {prems, ...} =>
+ Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
let
- val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
+ val cnfx_thms = map (make_cnfx_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
in
cut_facts_tac cut_thms 1
--- a/src/HOL/Tools/reification.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/reification.ML Wed Jul 08 21:33:00 2015 +0200
@@ -23,11 +23,12 @@
val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp}
-fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn { concl, ... } =>
+fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn {context = ctxt', concl, ...} =>
let
- val ct = case some_t
- of NONE => Thm.dest_arg concl
- | SOME t => Thm.cterm_of ctxt t
+ val ct =
+ (case some_t of
+ NONE => Thm.dest_arg concl
+ | SOME t => Thm.cterm_of ctxt' t)
val thm = conv ct;
in
if Thm.is_reflexive thm then no_tac
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Wed Jul 08 19:28:43 2015 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Jul 08 21:33:00 2015 +0200
@@ -441,9 +441,8 @@
THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms exE}
THEN' eresolve_tac ctxt @{thms conjE}
THEN' REPEAT_DETERM o eresolve_tac ctxt @{thms Pair_inject}
- THEN' Subgoal.FOCUS (fn {prems, ...} =>
- (* FIXME inner context!? *)
- simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
+ THEN' Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
+ simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (filter is_eq prems)) 1) ctxt
THEN' TRY o assume_tac ctxt
in
case try mk_term (Thm.term_of ct) of