eq_assumption now uses aeconv instead of aconv.

--- a/src/Pure/thm.ML	Wed May 07 10:59:46 2008 +0200
+++ b/src/Pure/thm.ML	Wed May 07 10:59:47 2008 +0200
@@ -1241,7 +1241,7 @@
     val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
   in
-    (case find_index (op aconv) (Logic.assum_pairs (~1, Bi)) of
+    (case find_index Pattern.aeconv (Logic.assum_pairs (~1, Bi)) of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
         Thm {thy_ref = thy_ref,