# HG changeset patch
# User wenzelm
# Date 920977672 -3600
# Node ID 47c801a77f324376ea546f2229130504184d1afd
# Parent  6e4c7209ff396875d1043c59d40bacda58c12efc
pretty_thm_no_quote;

diff -r 6e4c7209ff39 -r 47c801a77f32 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Mar 09 12:07:32 1999 +0100
+++ b/src/Pure/display.ML	Tue Mar 09 12:07:52 1999 +0100
@@ -10,6 +10,7 @@
 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_thms	: thm list -> Pretty.T
   val string_of_thm	: thm -> string
@@ -46,13 +47,13 @@
 fun pretty_tag (name, args) = Pretty.strs (name :: args);
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
-fun pretty_thm th =
+fun pretty_thm_aux quote th =
   let
     val {sign, hyps, prop, ...} = rep_thm th;
     val xshyps = Thm.extra_shyps th;
     val (_, tags) = Thm.get_name_tags th;
 
-    val prt_term = Pretty.quote o Sign.pretty_term sign;
+    val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign;
 
     val hlen = length xshyps + length hyps;
     val hsymbs =
@@ -67,6 +68,9 @@
       else [Pretty.brk 1, pretty_tags tags];
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
+val pretty_thm_no_quote = pretty_thm_aux false;
+val pretty_thm = pretty_thm_aux true;
+
 val string_of_thm = Pretty.string_of o pretty_thm;
 val pprint_thm = Pretty.pprint o pretty_thm;