# HG changeset patch
# User wenzelm
# Date 1004032541 -7200
# Node ID c1c4890a1ecbf62a2b39a072595c777fc525f350
# Parent  a5d1c9b34900da1b687c02dd4ef9a71d59dcd0c8
check_goal: setmp proofs 0;

diff -r a5d1c9b34900 -r c1c4890a1ecb src/Pure/Isar/isar_thy.ML
--- 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;