removed pretty_thm_no_hyps (again);
authorwenzelm
Mon Jul 12 22:23:07 1999 +0200 (1999-07-12)
changeset 69763895ba31db71
parent 6975 42fbea767673
child 6977 4781c0673e83
removed pretty_thm_no_hyps (again);
src/Pure/display.ML
     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