# HG changeset patch
# User wenzelm
# Date 1126977454 -7200
# Node ID d008d04068a16a0e58403b9c774cfe0945181442
# Parent  e4cdb9f061fbe23176823011f94dc939caf770df
pretty_thm_aux: ora masked by quick_and_dirty;

diff -r e4cdb9f061fb -r d008d04068a1 src/Pure/display.ML
--- a/src/Pure/display.ML	Sat Sep 17 19:17:33 2005 +0200
+++ b/src/Pure/display.ML	Sat Sep 17 19:17:34 2005 +0200
@@ -77,16 +77,17 @@
     val prt_term = q o (Pretty.term pp);
 
     val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
+    val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
     val hlen = length xshyps + length hyps' + length tpairs;
     val hsymbs =
-      if hlen = 0 andalso not ora then []
+      if hlen = 0 andalso not ora' then []
       else if ! show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
           (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
            map (Pretty.sort pp) xshyps @
-            (if ora then [Pretty.str "!"] else []))]
+            (if ora' then [Pretty.str "!"] else []))]
       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
-        (if ora then "!" else "") ^ "]")];
+        (if ora' then "!" else "") ^ "]")];
     val tsymbs =
       if null tags orelse not (! show_tags) then []
       else [Pretty.brk 1, pretty_tags tags];