src/Pure/display.ML
changeset 32738 15bb09ca0378
parent 32433 11661f4327bb
child 32784 1a5dde5079ac
--- 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*)