type thm: fully internal derivation, no longer exported;

--- a/src/FOL/ex/IffOracle.thy	Mon Sep 22 13:56:04 2008 +0200
+++ b/src/FOL/ex/IffOracle.thy	Mon Sep 22 15:26:07 2008 +0200
@@ -35,7 +35,7 @@
 
 ML {* iff_oracle (@{theory}, 2) *}
 ML {* iff_oracle (@{theory}, 10) *}
-ML {* #der (Thm.rep_thm (iff_oracle (@{theory}, 10))) *}
+ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
 
 text {* These oracle calls had better fail. *}
 

--- 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 []