src/Pure/Pure.thy

   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"
   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" == ""
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"