src/Pure/old_goals.ML
changeset 32738 15bb09ca0378
parent 32432 64f30bdd3ba1
child 32957 675c0c7e6a37
     1.1 --- a/src/Pure/old_goals.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    type proof
     1.5    val premises: unit -> thm list
     1.6    val reset_goals: unit -> unit
     1.7 -  val result_error_fn: (thm -> string -> thm) ref
     1.8 +  val result_error_fn: (thm -> string -> thm) Unsynchronized.ref
     1.9    val print_sign_exn: theory -> exn -> 'a
    1.10    val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
    1.11    val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm
    1.12 @@ -233,21 +233,21 @@
    1.13  (*** References ***)
    1.14  
    1.15  (*Current assumption list -- set by "goal".*)
    1.16 -val curr_prems = ref([] : thm list);
    1.17 +val curr_prems = Unsynchronized.ref([] : thm list);
    1.18  
    1.19  (*Return assumption list -- useful if you didn't save "goal"'s result. *)
    1.20  fun premises() = !curr_prems;
    1.21  
    1.22  (*Current result maker -- set by "goal", used by "result".  *)
    1.23  fun init_mkresult _ = error "No goal has been supplied in subgoal module";
    1.24 -val curr_mkresult = ref (init_mkresult: bool*thm->thm);
    1.25 +val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm);
    1.26  
    1.27  (*List of previous goal stacks, for the undo operation.  Set by setstate.
    1.28    A list of lists!*)
    1.29 -val undo_list = ref([[(asm_rl, Seq.empty)]] : gstack list);
    1.30 +val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list);
    1.31  
    1.32  (* Stack of proof attempts *)
    1.33 -val proofstack = ref([]: proof list);
    1.34 +val proofstack = Unsynchronized.ref([]: proof list);
    1.35  
    1.36  (*reset all refs*)
    1.37  fun reset_goals () =
    1.38 @@ -272,7 +272,7 @@
    1.39        Goal_Display.pretty_goals_without_context (!goals_limit) state @
    1.40      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
    1.41  
    1.42 -val result_error_fn = ref result_error_default;
    1.43 +val result_error_fn = Unsynchronized.ref result_error_default;
    1.44  
    1.45  
    1.46  (*Common treatment of "goal" and "prove_goal":