author | oheimb |
Wed, 27 Oct 1999 11:12:10 +0200 | |
changeset 7942 | 4f8cf6552787 |
parent 7941 | 653964583bd3 |
child 7943 | e31a3c0c2c1e |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- 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 ***)