# HG changeset patch
# User wenzelm
# Date 934905095 -7200
# Node ID 1ba436add81b5995c05d5eb20a3be4c2bc8c5e4e
# Parent  75cc3a327bd4cbd6f395dce7b456b0f601d06b08
reset_goals;

diff -r 75cc3a327bd4 -r 1ba436add81b src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue Aug 17 17:34:43 1999 +0200
+++ b/src/Pure/goals.ML	Tue Aug 17 17:51:35 1999 +0200
@@ -12,6 +12,7 @@
 signature GOALS =
   sig
   type proof
+  val reset_goals       : unit -> unit
   val atomic_goal	: theory -> string -> thm list
   val atomic_goalw	: theory -> thm list -> string -> thm list
   val Goal		: string -> thm list
@@ -100,9 +101,8 @@
 fun premises() = !curr_prems;
 
 (*Current result maker -- set by "goal", used by "result".  *)
-val curr_mkresult = 
-    ref((fn _=> error"No goal has been supplied in subgoal module") 
-       : bool*thm->thm);
+fun init_mkresult _ = error "No goal has been supplied in subgoal module";
+val curr_mkresult = ref (init_mkresult: bool*thm->thm);
 
 val dummy = trivial(read_cterm (Theory.sign_of ProtoPure.thy)
     ("PROP No_goal_has_been_supplied",propT));
@@ -114,6 +114,11 @@
 (* Stack of proof attempts *)
 val proofstack = ref([]: proof list);
 
+(*reset all refs*)
+fun reset_goals () =
+  (curr_prems := []; curr_mkresult := init_mkresult;
+    undo_list := [[(dummy, Seq.empty)]]; proofstack := []);
+
 
 (*** Setting up goal-directed proof ***)