diff -r d3cf88fe77bc -r b17d863a050f src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Sep 22 13:56:04 2008 +0200
+++ b/src/Pure/display.ML	Mon Sep 22 15:26:07 2008 +0200
@@ -61,7 +61,7 @@
 fun pretty_thm_aux pp quote show_hyps' asms raw_th =
   let
     val th = Thm.strip_shyps raw_th;
-    val {hyps, tpairs, prop, der, ...} = Thm.rep_thm th;
+    val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
     val xshyps = Thm.extra_shyps th;
     val tags = Thm.get_tags th;
 
@@ -69,7 +69,7 @@
     val prt_term = q o Pretty.term pp;
 
     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
-    val ora' = Deriv.oracle_of der andalso (! show_hyps orelse not (! quick_and_dirty));
+    val ora' = Thm.oracle_of th 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 []