src/Pure/display.ML
changeset 32738 15bb09ca0378
parent 32433 11661f4327bb
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/display.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -7,10 +7,10 @@
     1.4  
     1.5  signature BASIC_DISPLAY =
     1.6  sig
     1.7 -  val goals_limit: int ref
     1.8 -  val show_consts: bool ref
     1.9 -  val show_hyps: bool ref
    1.10 -  val show_tags: bool ref
    1.11 +  val goals_limit: int Unsynchronized.ref
    1.12 +  val show_consts: bool Unsynchronized.ref
    1.13 +  val show_hyps: bool Unsynchronized.ref
    1.14 +  val show_tags: bool Unsynchronized.ref
    1.15  end;
    1.16  
    1.17  signature DISPLAY =
    1.18 @@ -39,8 +39,8 @@
    1.19  val goals_limit = Goal_Display.goals_limit;
    1.20  val show_consts = Goal_Display.show_consts;
    1.21  
    1.22 -val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    1.23 -val show_tags = ref false;      (*false: suppress tags*)
    1.24 +val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)
    1.25 +val show_tags = Unsynchronized.ref false;    (*false: suppress tags*)
    1.26  
    1.27  
    1.28