--- 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":