# HG changeset patch
# User wenzelm
# Date 1154000584 -7200
# Node ID 6ea469c0331417ea799c9f8af21142a1c7d58e3d
# Parent  4b8e42490e5880b5aa45705d5d471304657dde67
removed obsolete pretty_thm_no_quote;

diff -r 4b8e42490e58 -r 6ea469c03314 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Jul 27 13:43:03 2006 +0200
+++ b/src/Pure/display.ML	Thu Jul 27 13:43:04 2006 +0200
@@ -33,7 +33,6 @@
   val raw_string_of_term: term -> string
   val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
-  val pretty_thm_no_quote: thm -> Pretty.T
   val pretty_thm: thm -> Pretty.T
   val pretty_thms: thm list -> Pretty.T
   val pretty_thm_sg: theory -> thm -> Pretty.T
@@ -100,12 +99,8 @@
       else [Pretty.brk 1, pretty_tags tags];
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
-fun gen_pretty_thm quote th =
-  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote false [] th;
-
-val pretty_thm = gen_pretty_thm true;
-val pretty_thm_no_quote = gen_pretty_thm false;
-
+fun pretty_thm th =
+  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) true false [] th;
 
 val string_of_thm = Pretty.string_of o pretty_thm;