author | wenzelm |
Sat, 17 Sep 2005 18:11:28 +0200 | |
changeset 17468 | 7c040a5fd171 |
parent 17467 | 2e9f745924d0 |
child 17469 | 4524bf3026d3 |
--- a/src/Pure/display.ML Sat Sep 17 18:11:27 2005 +0200 +++ b/src/Pure/display.ML Sat Sep 17 18:11:28 2005 +0200 @@ -76,7 +76,7 @@ val q = if quote then Pretty.quote else I; val prt_term = q o (Pretty.term pp); - val hyps' = if ! show_hyps then hyps else fold (remove (op =)) asms hyps; + val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps; val hlen = length xshyps + length hyps' + length tpairs; val hsymbs = if hlen = 0 andalso not ora then []