# HG changeset patch
# User berghofe
# Date 1210150787 -7200
# Node ID 46b90bbc370dd913612659495bd315e220f379aa
# Parent  6c3eec8157d397bc9909ed4ecf22433e756df2ce
eq_assumption now uses aeconv instead of aconv.

diff -r 6c3eec8157d3 -r 46b90bbc370d src/Pure/thm.ML
--- 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,