# HG changeset patch # User wenzelm # Date 1126977454 -7200 # Node ID d008d04068a16a0e58403b9c774cfe0945181442 # Parent e4cdb9f061fbe23176823011f94dc939caf770df pretty_thm_aux: ora masked by quick_and_dirty; diff -r e4cdb9f061fb -r d008d04068a1 src/Pure/display.ML --- a/src/Pure/display.ML Sat Sep 17 19:17:33 2005 +0200 +++ b/src/Pure/display.ML Sat Sep 17 19:17:34 2005 +0200 @@ -77,16 +77,17 @@ val prt_term = q o (Pretty.term pp); val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps; + val ora' = ora 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 [] + if hlen = 0 andalso not ora' then [] else if ! show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @ map (Pretty.sort pp) xshyps @ - (if ora then [Pretty.str "!"] else []))] + (if ora' then [Pretty.str "!"] else []))] else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ - (if ora then "!" else "") ^ "]")]; + (if ora' then "!" else "") ^ "]")]; val tsymbs = if null tags orelse not (! show_tags) then [] else [Pretty.brk 1, pretty_tags tags];