diff -r fc45401bdf6f -r 9ba30eeec7ce src/Pure/display.ML
--- a/src/Pure/display.ML	Sat Nov 15 21:31:20 2008 +0100
+++ b/src/Pure/display.ML	Sat Nov 15 21:31:21 2008 +0100
@@ -69,7 +69,10 @@
     val prt_term = q o Pretty.term pp;
 
     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
-    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty));
+(* FIXME
+    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *)
+    val ora' = false;
+
     val hlen = length xshyps + length hyps' + length tpairs;
     val hsymbs =
       if hlen = 0 andalso not ora' then []