1.1 --- a/src/Pure/display.ML	Wed May 20 18:55:41 1998 +0200
     1.2 +++ b/src/Pure/display.ML	Wed May 20 18:56:00 1998 +0200
     1.3 @@ -7,34 +7,34 @@
     1.4  *)
     1.5  
     1.6  signature DISPLAY =
     1.7 -  sig
     1.8 -  val pprint_cterm	: cterm -> pprint_args -> unit
     1.9 -  val pprint_ctyp	: ctyp -> pprint_args -> unit
    1.10 -  val pprint_theory	: theory -> pprint_args -> unit
    1.11 -  val pprint_thm	: thm -> pprint_args -> unit
    1.12 -  val pretty_ctyp	: ctyp -> Pretty.T
    1.13 -  val pretty_cterm	: cterm -> Pretty.T
    1.14 +sig
    1.15 +  val show_hyps		: bool ref
    1.16    val pretty_thm	: thm -> Pretty.T
    1.17 -  val print_cterm	: cterm -> unit
    1.18 -  val print_ctyp	: ctyp -> unit
    1.19 -  val show_consts	: bool ref
    1.20 -  val print_goals	: int -> thm -> unit
    1.21 -  val pretty_name_space : string * NameSpace.T -> Pretty.T
    1.22 -  val print_syntax	: theory -> unit
    1.23 -  val print_theory	: theory -> unit
    1.24 -  val print_data	: theory -> string -> unit
    1.25 +  val string_of_thm	: thm -> string
    1.26 +  val pprint_thm	: thm -> pprint_args -> unit
    1.27    val print_thm		: thm -> unit
    1.28    val prth		: thm -> thm
    1.29    val prthq		: thm Seq.seq -> thm Seq.seq
    1.30    val prths		: thm list -> thm list
    1.31 -  val show_hyps		: bool ref
    1.32 -  val string_of_cterm	: cterm -> string
    1.33 +  val pretty_ctyp	: ctyp -> Pretty.T
    1.34 +  val pprint_ctyp	: ctyp -> pprint_args -> unit
    1.35    val string_of_ctyp	: ctyp -> string
    1.36 -  val string_of_thm	: thm -> string
    1.37 -  end;
    1.38 +  val print_ctyp	: ctyp -> unit
    1.39 +  val pretty_cterm	: cterm -> Pretty.T
    1.40 +  val pprint_cterm	: cterm -> pprint_args -> unit
    1.41 +  val string_of_cterm	: cterm -> string
    1.42 +  val print_cterm	: cterm -> unit
    1.43 +  val pretty_theory	: theory -> Pretty.T
    1.44 +  val pprint_theory	: theory -> pprint_args -> unit
    1.45 +  val print_syntax	: theory -> unit
    1.46 +  val print_data	: theory -> string -> unit
    1.47 +  val print_theory	: theory -> unit
    1.48 +  val pretty_name_space : string * NameSpace.T -> Pretty.T
    1.49 +  val show_consts	: bool ref
    1.50 +  val print_goals	: int -> thm -> unit
    1.51 +end;
    1.52  
    1.53 -
    1.54 -structure Display : DISPLAY =
    1.55 +structure Display: DISPLAY =
    1.56  struct
    1.57  
    1.58  (*If false, hypotheses are printed as dots*)
    1.59 @@ -102,6 +102,7 @@
    1.60  
    1.61  (** print theory **)
    1.62  
    1.63 +val pretty_theory = Sign.pretty_sg o sign_of;
    1.64  val pprint_theory = Sign.pprint_sg o sign_of;
    1.65  
    1.66  val print_syntax = Syntax.print_syntax o syn_of;