# HG changeset patch
# User wenzelm
# Date 1126973488 -7200
# Node ID 7c040a5fd171acf90046b34e76d5c0e4bfd34b25
# Parent  2e9f745924d0514ee8180681a3c533affe423b29
pretty_thm_aux: aconv hyps;

diff -r 2e9f745924d0 -r 7c040a5fd171 src/Pure/display.ML
--- 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 []