reset_goals no longer empties the proof stack
authoroheimb
Wed, 27 Oct 1999 11:12:10 +0200
changeset 7942 4f8cf6552787
parent 7941 653964583bd3
child 7943 e31a3c0c2c1e
reset_goals no longer empties the proof stack
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 ***)