diff -r e77baf329f48 -r 82d4874757df src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 08 22:13:49 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -56,7 +56,7 @@
 
 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
 fun have_common_thm ths1 ths2 =
-  exists (member (untyped_aconv o pairself prop_of) ths1)
+  exists (member (metis_aconv_untyped o pairself prop_of) ths1)
          (map Meson.make_meta_clause ths2)
 
 (*Determining which axiom clauses are actually used*)