pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
authorwenzelm
Sat Nov 15 21:31:21 2008 +0100 (2008-11-15)
changeset 288029ba30eeec7ce
parent 28801 fc45401bdf6f
child 28803 d90258bbb18f
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sat Nov 15 21:31:20 2008 +0100
     1.2 +++ b/src/Pure/display.ML	Sat Nov 15 21:31:21 2008 +0100
     1.3 @@ -69,7 +69,10 @@
     1.4      val prt_term = q o Pretty.term pp;
     1.5  
     1.6      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
     1.7 -    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty));
     1.8 +(* FIXME
     1.9 +    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *)
    1.10 +    val ora' = false;
    1.11 +
    1.12      val hlen = length xshyps + length hyps' + length tpairs;
    1.13      val hsymbs =
    1.14        if hlen = 0 andalso not ora' then []