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

     2.1 --- a/src/Pure/display.ML	Mon Sep 22 13:56:04 2008 +0200
     2.2 +++ b/src/Pure/display.ML	Mon Sep 22 15:26:07 2008 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4  fun pretty_thm_aux pp quote show_hyps' asms raw_th =
     2.5    let
     2.6      val th = Thm.strip_shyps raw_th;
     2.7 -    val {hyps, tpairs, prop, der, ...} = Thm.rep_thm th;
     2.8 +    val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
     2.9      val xshyps = Thm.extra_shyps th;
    2.10      val tags = Thm.get_tags th;
    2.11  
    2.12 @@ -69,7 +69,7 @@
    2.13      val prt_term = q o Pretty.term pp;
    2.14  
    2.15      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    2.16 -    val ora' = Deriv.oracle_of der andalso (! show_hyps orelse not (! quick_and_dirty));
    2.17 +    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty));
    2.18      val hlen = length xshyps + length hyps' + length tpairs;
    2.19      val hsymbs =
    2.20        if hlen = 0 andalso not ora' then []