# HG changeset patch
# User wenzelm
# Date 930955257 -7200
# Node ID b92c2f0413b851f5f7a8e80264abe218db1c8d3e
# Parent  6e56603fb33942e8041d8513b23cb2695488755e
oops;

diff -r 6e56603fb339 -r b92c2f0413b8 src/Pure/display.ML
--- a/src/Pure/display.ML	Sat Jul 03 00:28:05 1999 +0200
+++ b/src/Pure/display.ML	Sat Jul 03 00:40:57 1999 +0200
@@ -63,14 +63,15 @@
     val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign;
 
     val hlen = length xshyps + length hyps;
+    val ex_ora = ex_oracle der;
     val hsymbs =
-      if hlen = 0 then []
+      if hlen = 0 andalso not ex_ora then []
       else if ! show_hyps then
         [Pretty.brk 2, Pretty.list "[" "]"
           (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps @
-            (if ex_oracle der then [Pretty.str "!"] else []))]
+            (if ex_ora then [Pretty.str "!"] else []))]
       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
-        (if ex_oracle der then "!" else "") ^ "]")];
+        (if ex_ora then "!" else "") ^ "]")];
     val tsymbs =
       if null tags orelse not (! show_tags) then []
       else [Pretty.brk 1, pretty_tags tags];