# HG changeset patch # User wenzelm # Date 1436383980 -7200 # Node ID 8304fb4fb823e21a0852f2e983c1d33c5a5e85a9 # Parent 757549b4bbe627c5150d4577ee8e765b05e415cd clarified context; diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/Meson/meson.ML --- 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*) diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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'] diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- 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; diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/SMT/smt_solver.ML --- 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 diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/cnf.ML --- 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 diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/reification.ML --- 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 diff -r 757549b4bbe6 -r 8304fb4fb823 src/HOL/Tools/set_comprehension_pointfree.ML --- 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