src/Pure/display.ML
changeset 28316 b17d863a050f
parent 28290 4cc2b6046258
child 28802 9ba30eeec7ce
     1.1 --- a/src/Pure/display.ML	Mon Sep 22 13:56:04 2008 +0200
     1.2 +++ b/src/Pure/display.ML	Mon Sep 22 15:26:07 2008 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  fun pretty_thm_aux pp quote show_hyps' asms raw_th =
     1.5    let
     1.6      val th = Thm.strip_shyps raw_th;
     1.7 -    val {hyps, tpairs, prop, der, ...} = Thm.rep_thm th;
     1.8 +    val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
     1.9      val xshyps = Thm.extra_shyps th;
    1.10      val tags = Thm.get_tags th;
    1.11  
    1.12 @@ -69,7 +69,7 @@
    1.13      val prt_term = q o Pretty.term pp;
    1.14  
    1.15      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    1.16 -    val ora' = Deriv.oracle_of der andalso (! show_hyps orelse not (! quick_and_dirty));
    1.17 +    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty));
    1.18      val hlen = length xshyps + length hyps' + length tpairs;
    1.19      val hsymbs =
    1.20        if hlen = 0 andalso not ora' then []