# HG changeset patch
# User wenzelm
# Date 1361356830 -3600
# Node ID 1973089f1dbacb5590a7e65fd39d1400511058de
# Parent  3fe0d8d55975ab164a2a3fd58671d7e3f4c7f460
proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);

diff -r 3fe0d8d55975 -r 1973089f1dba src/Pure/Isar/proof.ML
--- 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 ->
diff -r 3fe0d8d55975 -r 1973089f1dba src/Pure/Isar/toplevel.ML
--- 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