# HG changeset patch
# User wenzelm
# Date 931810987 -7200
# Node ID 3895ba31db711899d962a2af690b525ab26bb528
# Parent  42fbea7676737ea23c27e72a6c03f357ce7cb1c9
removed pretty_thm_no_hyps (again);

diff -r 42fbea767673 -r 3895ba31db71 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Jul 12 21:51:47 1999 +0200
+++ b/src/Pure/display.ML	Mon Jul 12 22:23:07 1999 +0200
@@ -10,9 +10,8 @@
 sig
   val show_hyps		: bool ref
   val show_tags		: bool ref
+  val pretty_thm_no_quote: thm -> Pretty.T
   val pretty_thm	: thm -> Pretty.T
-  val pretty_thm_no_quote: thm -> Pretty.T
-  val pretty_thm_no_hyps: thm -> Pretty.T
   val pretty_thms	: thm list -> Pretty.T
   val string_of_thm	: thm -> string
   val pprint_thm	: thm -> pprint_args -> unit
@@ -82,7 +81,6 @@
 
 val pretty_thm = pretty_thm_aux true;
 val pretty_thm_no_quote = pretty_thm_aux false;
-val pretty_thm_no_hyps = setmp show_hyps false pretty_thm;
 
 end;