# HG changeset patch
# User wenzelm
# Date 1415554063 -3600
# Node ID 114255dce178f100e20277361774abe01aaab21b
# Parent  c9e744ea8a3815a4d7a6aa3ab6a0ed14b0c0b09d
proper context;

diff -r c9e744ea8a38 -r 114255dce178 src/HOL/HOL.thy
--- 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
 
diff -r c9e744ea8a38 -r 114255dce178 src/Provers/blast.ML
--- 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
diff -r c9e744ea8a38 -r 114255dce178 src/Provers/classical.ML
--- 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,
diff -r c9e744ea8a38 -r 114255dce178 src/Provers/hypsubst.ML
--- 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