proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);

--- a/src/Pure/Isar/proof.ML	Wed Feb 20 00:00:42 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Feb 20 11:40:30 2013 +0100
@@ -114,6 +114,7 @@
   val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
+  val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
   val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
   val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->

--- a/src/Pure/Isar/toplevel.ML	Wed Feb 20 00:00:42 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Feb 20 11:40:30 2013 +0100
@@ -694,7 +694,8 @@
 
 fun proof_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
-    if immediate orelse null proof_trs orelse not (can proof_of st')
+    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
+      Proof.is_relevant (proof_of st')
     then
       let val (results, st'') = fold_map command_result proof_trs st'
       in (Future.value ((tr, st') :: results), st'') end