diff -r 010eefa0a4f3 -r 7a86358a3c0b src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/Provers/classical.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -166,7 +166,13 @@
   else rule;
 
 (*flatten nested meta connectives in prems*)
-val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
+fun flat_rule opt_context th =
+  let
+    val ctxt =
+      (case opt_context of
+        NONE => Proof_Context.init_global (Thm.theory_of_thm th)
+      | SOME context => Context.proof_of context);
+  in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
 
 
 (*** Useful tactics for classical reasoning ***)
@@ -325,7 +331,7 @@
   if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   else
     let
-      val th' = flat_rule th;
+      val th' = flat_rule context th;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition Thm.no_prems [th'];
       val nI = Item_Net.length safeIs + 1;
@@ -354,7 +360,7 @@
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
-      val th' = classical_rule (flat_rule th);
+      val th' = classical_rule (flat_rule context th);
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition (fn rl => nprems_of rl=1) [th'];
       val nI = Item_Net.length safeIs;
@@ -386,7 +392,7 @@
   if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   else
     let
-      val th' = flat_rule th;
+      val th' = flat_rule context th;
       val nI = Item_Net.length hazIs + 1;
       val nE = Item_Net.length hazEs;
       val _ = warn_claset context th cs;
@@ -415,7 +421,7 @@
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
-      val th' = classical_rule (flat_rule th);
+      val th' = classical_rule (flat_rule context th);
       val nI = Item_Net.length hazIs;
       val nE = Item_Net.length hazEs + 1;
       val _ = warn_claset context th cs;
@@ -443,12 +449,12 @@
         to insert.
 ***)
 
-fun delSI th
+fun delSI context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeIs th then
     let
-      val th' = flat_rule th;
+      val th' = flat_rule context th;
       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
     in
       CS
@@ -466,12 +472,12 @@
     end
   else cs;
 
-fun delSE th
+fun delSE context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeEs th then
     let
-      val th' = classical_rule (flat_rule th);
+      val th' = classical_rule (flat_rule context th);
       val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
     in
       CS
@@ -493,7 +499,7 @@
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazIs th then
-    let val th' = flat_rule th in
+    let val th' = flat_rule context th in
       CS
        {haz_netpair = delete ([th'], []) haz_netpair,
         dup_netpair = delete ([dup_intr th'], []) dup_netpair,
@@ -511,11 +517,11 @@
   handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
     error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
 
-fun delE th
+fun delE context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazEs th then
-    let val th' = classical_rule (flat_rule th) in
+    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,
@@ -537,7 +543,11 @@
     if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
       Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
       Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
-    then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
+    then
+      delSI context th
+        (delSE context th
+          (delI context th
+            (delE context th (delSE context th' (delE context th' cs)))))
     else (warn_thm context "Undeclared classical rule\n" th; cs)
   end;
 
@@ -774,24 +784,24 @@
 
 (*Dumb but fast*)
 fun fast_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
+  Object_Logic.atomize_prems_tac ctxt THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 (*Slower but smarter than fast_tac*)
 fun best_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
 
 (*even a bit smarter than best_tac*)
 fun first_best_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
 
 fun slow_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
 
 fun slow_best_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
 
 
@@ -800,13 +810,13 @@
 val weight_ASTAR = 5;
 
 fun astar_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
       (step_tac ctxt 1));
 
 fun slow_astar_tac ctxt =
-  Object_Logic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
       (slow_step_tac ctxt 1));
@@ -901,12 +911,12 @@
   in
     fn st => Seq.maps (fn rule => rtac rule i st) ruleq
   end)
-  THEN_ALL_NEW Goal.norm_hhf_tac;
+  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
 
 in
 
 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
-  | rule_tac _ rules facts = Method.rule_tac rules facts;
+  | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
 
 fun default_tac ctxt rules facts =
   HEADGOAL (rule_tac ctxt rules facts) ORELSE
@@ -941,7 +951,7 @@
     (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
     "apply some intro/elim rule (potentially classical)" #>
   Method.setup @{binding contradiction}
-    (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim])))
+    (Scan.succeed (fn ctxt => Method.rule ctxt [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))
     "proof by contradiction" #>
   Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac))
     "repeatedly apply safe steps" #>