src/Pure/display.ML

--- a/src/Pure/display.ML	Fri Sep 03 10:58:11 2010 +0200
+++ b/src/Pure/display.ML	Fri Sep 03 11:21:58 2010 +0200
@@ -8,7 +8,8 @@
 signature BASIC_DISPLAY =
 sig
   val goals_limit: int Unsynchronized.ref
-  val show_consts: bool Unsynchronized.ref
+  val show_consts_default: bool Unsynchronized.ref
+  val show_consts: bool Config.T
   val show_hyps: bool Unsynchronized.ref
   val show_tags: bool Unsynchronized.ref
 end;
@@ -37,6 +38,7 @@
 (** options **)
 
 val goals_limit = Goal_Display.goals_limit;
+val show_consts_default = Goal_Display.show_consts_default;
 val show_consts = Goal_Display.show_consts;
 
 val show_hyps = Unsynchronized.ref false;    (*false: print meta-hypotheses as dots*)