src/Pure/display.ML
changeset 6976 3895ba31db71
parent 6926 7ffc131909e5
child 7067 601f930d3739
     1.1 --- a/src/Pure/display.ML	Mon Jul 12 21:51:47 1999 +0200
     1.2 +++ b/src/Pure/display.ML	Mon Jul 12 22:23:07 1999 +0200
     1.3 @@ -10,9 +10,8 @@
     1.4  sig
     1.5    val show_hyps		: bool ref
     1.6    val show_tags		: bool ref
     1.7 +  val pretty_thm_no_quote: thm -> Pretty.T
     1.8    val pretty_thm	: thm -> Pretty.T
     1.9 -  val pretty_thm_no_quote: 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 @@ -82,7 +81,6 @@
    1.15  
    1.16  val pretty_thm = pretty_thm_aux true;
    1.17  val pretty_thm_no_quote = pretty_thm_aux false;
    1.18 -val pretty_thm_no_hyps = setmp show_hyps false pretty_thm;
    1.19  
    1.20  end;
    1.21