# HG changeset patch # User wenzelm # Date 1226781081 -3600 # Node ID 9ba30eeec7ce7333d6d98c55a3077418b44f83e5 # Parent fc45401bdf6f28340126a17efd799f1a42857548 pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises); diff -r fc45401bdf6f -r 9ba30eeec7ce src/Pure/display.ML --- a/src/Pure/display.ML Sat Nov 15 21:31:20 2008 +0100 +++ b/src/Pure/display.ML Sat Nov 15 21:31:21 2008 +0100 @@ -69,7 +69,10 @@ val prt_term = q o Pretty.term pp; val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps; - val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); +(* FIXME + val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *) + val ora' = false; + val hlen = length xshyps + length hyps' + length tpairs; val hsymbs = if hlen = 0 andalso not ora' then []