--- 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;