--- a/src/Pure/display.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/display.ML Tue Sep 29 11:49:22 2009 +0200
@@ -7,10 +7,10 @@
signature BASIC_DISPLAY =
sig
- val goals_limit: int ref
- val show_consts: bool ref
- val show_hyps: bool ref
- val show_tags: bool ref
+ val goals_limit: int Unsynchronized.ref
+ val show_consts: bool Unsynchronized.ref
+ val show_hyps: bool Unsynchronized.ref
+ val show_tags: bool Unsynchronized.ref
end;
signature DISPLAY =
@@ -39,8 +39,8 @@
val goals_limit = Goal_Display.goals_limit;
val show_consts = Goal_Display.show_consts;
-val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
-val show_tags = ref false; (*false: suppress tags*)
+val show_hyps = Unsynchronized.ref false; (*false: print meta-hypotheses as dots*)
+val show_tags = Unsynchronized.ref false; (*false: suppress tags*)