check_goal: setmp proofs 0;

--- a/src/Pure/Isar/isar_thy.ML	Thu Oct 25 16:09:39 2001 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 25 19:55:41 2001 +0200
@@ -389,6 +389,7 @@
         val check =
           (fn () => Seq.pull (SkipProof.local_skip_proof (K (), fn thm => rule := Some thm) state))
           |> Library.setmp quick_and_dirty true
+          |> Library.setmp proofs 0
           |> Library.transform_error;
         val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
       in (case result of (Some _, None) => () | (_, exn) => warn exn); state end;