--- a/src/Pure/Isar/toplevel.ML Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Apr 10 21:31:05 2012 +0200
@@ -672,12 +672,7 @@
fun proof_result immediate (tr, proof_trs) st =
let val st' = command tr st in
- if immediate orelse
- null proof_trs orelse
- Keyword.is_schematic_goal (name_of tr) orelse
- exists (Keyword.is_qed_global o name_of) proof_trs orelse
- not (can proof_of st') orelse
- Proof.is_relevant (proof_of st')
+ if immediate orelse null proof_trs orelse not (can proof_of st')
then
let val (states, st'') = fold_map command_result proof_trs st'
in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end