pretty_thm_aux: aconv hyps;
authorwenzelm
Sat Sep 17 18:11:28 2005 +0200 (2005-09-17)
changeset 174687c040a5fd171
parent 17467 2e9f745924d0
child 17469 4524bf3026d3
pretty_thm_aux: aconv hyps;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sat Sep 17 18:11:27 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Sep 17 18:11:28 2005 +0200
     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 =)) asms hyps;
     1.8 +    val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
     1.9      val hlen = length xshyps + length hyps' + length tpairs;
    1.10      val hsymbs =
    1.11        if hlen = 0 andalso not ora then []