# HG changeset patch
# User oheimb
# Date 941015530 -7200
# Node ID 4f8cf6552787d73027cdf0f0efc7fef53b900847
# Parent  653964583bd3471c85f4f0663cbd7d88f07ae1b9
reset_goals no longer empties the proof stack

diff -r 653964583bd3 -r 4f8cf6552787 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Oct 26 22:37:34 1999 +0200
+++ b/src/Pure/goals.ML	Wed Oct 27 11:12:10 1999 +0200
@@ -117,7 +117,7 @@
 (*reset all refs*)
 fun reset_goals () =
   (curr_prems := []; curr_mkresult := init_mkresult;
-    undo_list := [[(dummy, Seq.empty)]]; proofstack := []);
+    undo_list := [[(dummy, Seq.empty)]]);
 
 
 (*** Setting up goal-directed proof ***)