src/Pure/display.ML

 Printing of theorems, results etc.
 *)
 
 signature BASIC_DISPLAY =
 sig
-  val goals_limit: int 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;

 structure Display: DISPLAY =
 struct
 
 (** 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*)
 val show_tags = Unsynchronized.ref false;    (*false: suppress tags*)