# HG changeset patch
# User wenzelm
# Date 1272310604 -7200
# Node ID aaa9933039b3a7674f17ec39e866cdc29caf71c3
# Parent  bbd742107f56e091d5d3623e9bf3495423272e71
proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;

diff -r bbd742107f56 -r aaa9933039b3 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