1.1 --- a/src/Pure/display.ML	Thu Jul 08 18:28:02 1999 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Jul 08 18:29:07 1999 +0200
     1.3 @@ -10,8 +10,9 @@
     1.4  sig
     1.5    val show_hyps		: bool ref
     1.6    val show_tags		: bool ref
     1.7 +  val pretty_thm	: thm -> Pretty.T
     1.8    val pretty_thm_no_quote: thm -> Pretty.T
     1.9 -  val pretty_thm	: thm -> Pretty.T
    1.10 +  val pretty_thm_no_hyps: thm -> Pretty.T
    1.11    val pretty_thms	: thm list -> Pretty.T
    1.12    val string_of_thm	: thm -> string
    1.13    val pprint_thm	: thm -> pprint_args -> unit
    1.14 @@ -79,8 +80,9 @@
    1.15  
    1.16  in
    1.17  
    1.18 +val pretty_thm = pretty_thm_aux true;
    1.19  val pretty_thm_no_quote = pretty_thm_aux false;
    1.20 -val pretty_thm = pretty_thm_aux true;
    1.21 +val pretty_thm_no_hyps = setmp show_hyps false pretty_thm;
    1.22  
    1.23  end;
    1.24