--- 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