--- a/src/HOL/HOL.thy Sun Nov 09 17:04:14 2014 +0100
+++ b/src/HOL/HOL.thy Sun Nov 09 18:27:43 2014 +0100
@@ -905,7 +905,7 @@
apply (rule ex1E [OF major])
apply (rule prem)
apply (tactic {* ares_tac @{thms allI} 1 *})+
-apply (tactic {* eresolve_tac [Classical.dup_elim @{thm allE}] 1 *})
+apply (tactic {* eresolve_tac [Classical.dup_elim NONE @{thm allE}] 1 *})
apply iprover
done
--- a/src/Provers/blast.ML Sun Nov 09 17:04:14 2014 +0100
+++ b/src/Provers/blast.ML Sun Nov 09 18:27:43 2014 +0100
@@ -461,7 +461,7 @@
(*Like dup_elim, but puts the duplicated major premise FIRST*)
-fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
+fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
(*Rotate the assumptions in all new subgoals for the LIFO discipline*)
@@ -498,7 +498,7 @@
let val thy = Proof_Context.theory_of ctxt
val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars
fun tac (upd, dup,rot) i =
- emtac ctxt upd (if dup then rev_dup_elim rl else rl) i
+ emtac ctxt upd (if dup then rev_dup_elim ctxt rl else rl) i
THEN
rot_subgoals_tac (rot, #2 trl) i
in Option.SOME (trl, tac) end
--- a/src/Provers/classical.ML Sun Nov 09 17:04:14 2014 +0100
+++ b/src/Provers/classical.ML Sun Nov 09 18:27:43 2014 +0100
@@ -72,7 +72,7 @@
val deepen_tac: Proof.context -> int -> int -> tactic
val contr_tac: int -> tactic
- val dup_elim: thm -> thm
+ val dup_elim: Context.generic option -> thm -> thm
val dup_intr: thm -> thm
val dup_step_tac: Proof.context -> int -> tactic
val eq_mp_tac: Proof.context -> int -> tactic
@@ -205,10 +205,13 @@
(*Duplication of hazardous rules, for complete provers*)
fun dup_intr th = zero_var_indexes (th RS Data.classical);
-fun dup_elim th = (* FIXME proper context!? *)
+fun dup_elim context th =
let
- val rl = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
- val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
+ val ctxt =
+ (case context of
+ SOME c => Context.proof_of c
+ | NONE => Proof_Context.init_global (Thm.theory_of_thm th));
+ val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
@@ -428,7 +431,7 @@
CS
{hazEs = Item_Net.update th hazEs,
haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
- dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
+ dup_netpair = insert (nI, nE) ([], [dup_elim context th']) dup_netpair,
safeIs = safeIs,
safeEs = safeEs,
hazIs = hazIs,
@@ -523,7 +526,7 @@
let val th' = classical_rule (flat_rule context th) in
CS
{haz_netpair = delete ([], [th']) haz_netpair,
- dup_netpair = delete ([], [dup_elim th']) dup_netpair,
+ dup_netpair = delete ([], [dup_elim context th']) dup_netpair,
safeIs = safeIs,
safeEs = safeEs,
hazIs = hazIs,
--- a/src/Provers/hypsubst.ML Sun Nov 09 17:04:14 2014 +0100
+++ b/src/Provers/hypsubst.ML Sun Nov 09 18:27:43 2014 +0100
@@ -196,8 +196,8 @@
val imp_intr_tac = resolve_tac [Data.imp_intr];
-fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd;
-val dup_subst = rev_dup_elim ssubst
+fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
+fun dup_subst ctxt = rev_dup_elim ctxt ssubst
(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
(* premises containing meta-implications or quantifiers *)
@@ -207,7 +207,7 @@
fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) =>
let val n = length(Logic.strip_assums_hyp Bi) - 1
val (k, (orient, is_free)) = eq_var bnd false true Bi
- val rl = if is_free then dup_subst else ssubst
+ val rl = if is_free then dup_subst ctxt else ssubst
val rl = if orient then rl else Data.sym RS rl
in
DETERM