
diff -r e12f16366957 -r e58ca0311c0f src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 11 18:52:30 2013 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 11 20:16:28 2013 +0200
@@ -68,7 +68,8 @@
   and "}" :: prf_close % "proof"
   and "next" :: prf_block % "proof"
   and "qed" :: qed_block % "proof"
-  and "by" ".." "." "done" "sorry" :: "qed" % "proof"
+  and "by" ".." "." "sorry" :: "qed" % "proof"
+  and "done" :: "qed_script" % "proof"
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
   and "apply_end" :: prf_script % "proof" == ""




