src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Mon Apr 26 20:30:50 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Apr 26 21:36:44 2010 +0200
@@ -661,6 +661,7 @@
     if immediate orelse
       null proof_trs orelse
       OuterKeyword.is_schematic_goal (name_of tr) orelse
+      exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
       not (can proof_of st') orelse
       Proof.is_relevant (proof_of st')
     then