src/Pure/display.ML
changeset 19300 7689f81f8996
parent 18980 fd6b42e6bf50
child 19365 4fd1246d7998
equal deleted inserted replaced
19299:5f0610aafc48 19300:7689f81f8996
    74     val (_, tags) = Thm.get_name_tags th;
    74     val (_, tags) = Thm.get_name_tags th;
    75 
    75 
    76     val q = if quote then Pretty.quote else I;
    76     val q = if quote then Pretty.quote else I;
    77     val prt_term = q o (Pretty.term pp);
    77     val prt_term = q o (Pretty.term pp);
    78 
    78 
    79     val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
    79     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    80     val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
    80     val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
    81     val hlen = length xshyps + length hyps' + length tpairs;
    81     val hlen = length xshyps + length hyps' + length tpairs;
    82     val hsymbs =
    82     val hsymbs =
    83       if hlen = 0 andalso not ora' then []
    83       if hlen = 0 andalso not ora' then []
    84       else if ! show_hyps orelse show_hyps' then
    84       else if ! show_hyps orelse show_hyps' then