src/Pure/Isar/proof.ML
changeset 32738 15bb09ca0378
parent 32193 c314b4836031
child 32769 511e6976f031
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -30,8 +30,8 @@
     1.4    val enter_forward: state -> state
     1.5    val goal_message: (unit -> Pretty.T) -> state -> state
     1.6    val get_goal: state -> context * (thm list * thm)
     1.7 -  val show_main_goal: bool ref
     1.8 -  val verbose: bool ref
     1.9 +  val show_main_goal: bool Unsynchronized.ref
    1.10 +  val verbose: bool Unsynchronized.ref
    1.11    val pretty_state: int -> state -> Pretty.T list
    1.12    val pretty_goals: bool -> state -> Pretty.T list
    1.13    val refine: Method.text -> state -> state Seq.seq
    1.14 @@ -315,7 +315,7 @@
    1.15  
    1.16  (** pretty_state **)
    1.17  
    1.18 -val show_main_goal = ref false;
    1.19 +val show_main_goal = Unsynchronized.ref false;
    1.20  val verbose = ProofContext.verbose;
    1.21  
    1.22  fun pretty_facts _ _ NONE = []
    1.23 @@ -930,8 +930,8 @@
    1.24  
    1.25  fun gen_show prep_att prepp before_qed after_qed stmt int state =
    1.26    let
    1.27 -    val testing = ref false;
    1.28 -    val rule = ref (NONE: thm option);
    1.29 +    val testing = Unsynchronized.ref false;
    1.30 +    val rule = Unsynchronized.ref (NONE: thm option);
    1.31      fun fail_msg ctxt =
    1.32        "Local statement will fail to refine any pending goal" ::
    1.33        (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])