src/Pure/display.ML
changeset 19300 7689f81f8996
parent 18980 fd6b42e6bf50
child 19365 4fd1246d7998
     1.1 --- a/src/Pure/display.ML	Tue Mar 21 12:18:06 2006 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Mar 21 12:18:07 2006 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4      val q = if quote then Pretty.quote else I;
     1.5      val prt_term = q o (Pretty.term pp);
     1.6  
     1.7 -    val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
     1.8 +    val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
     1.9      val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
    1.10      val hlen = length xshyps + length hyps' + length tpairs;
    1.11      val hsymbs =