# HG changeset patch
# User wenzelm
# Date 931451347 -7200
# Node ID 7ffc131909e5ea350bbe587b4afc8e5434abf68f
# Parent  8d4d45ec6a3df6a20f86734259dfa113c989d084
added pretty_thm_no_hyps;

diff -r 8d4d45ec6a3d -r 7ffc131909e5 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Jul 08 18:28:02 1999 +0200
+++ b/src/Pure/display.ML	Thu Jul 08 18:29:07 1999 +0200
@@ -10,8 +10,9 @@
 sig
   val show_hyps		: bool ref
   val show_tags		: bool ref
+  val pretty_thm	: thm -> Pretty.T
   val pretty_thm_no_quote: thm -> Pretty.T
-  val pretty_thm	: 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
@@ -79,8 +80,9 @@
 
 in
 
+val pretty_thm = pretty_thm_aux true;
 val pretty_thm_no_quote = pretty_thm_aux false;
-val pretty_thm = pretty_thm_aux true;
+val pretty_thm_no_hyps = setmp show_hyps false pretty_thm;
 
 end;