src/Pure/old_goals.ML

--- a/src/Pure/old_goals.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/old_goals.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -19,7 +19,7 @@
   type proof
   val premises: unit -> thm list
   val reset_goals: unit -> unit
-  val result_error_fn: (thm -> string -> thm) ref
+  val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
   val print_sign_exn: theory -> exn -> 'a
   val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
   val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
@@ -233,21 +233,21 @@
 (*** References ***)
 
 (*Current assumption list -- set by "goal".*)
-val curr_prems = ref([] : thm list);
+val curr_prems = Unsynchronized.ref([] : thm list);
 
 (*Return assumption list -- useful if you didn't save "goal"'s result. *)
 fun premises() = !curr_prems;
 
 (*Current result maker -- set by "goal", used by "result".  *)
 fun init_mkresult _ = error "No goal has been supplied in subgoal module";
-val curr_mkresult = ref (init_mkresult: bool*thm->thm);
+val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
 
 (*List of previous goal stacks, for the undo operation.  Set by setstate.
   A list of lists!*)
-val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
+val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
 
 (* Stack of proof attempts *)
-val proofstack = ref([]: proof list);
+val proofstack = Unsynchronized.ref([]: proof list);
 
 (*reset all refs*)
 fun reset_goals () =
@@ -272,7 +272,7 @@
       Goal_Display.pretty_goals_without_context (!goals_limit) state @
     [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
 
-val result_error_fn = ref result_error_default;
+val result_error_fn = Unsynchronized.ref result_error_default;
 
 
 (*Common treatment of "goal" and "prove_goal":