--- a/src/Pure/display.ML Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/display.ML Tue Mar 21 12:18:07 2006 +0100
@@ -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 aconv)) asms hyps;
+ val hyps' = if ! show_hyps then hyps else subtract (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 =