Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_tactics.ML
changeset 43298 82d4874757df
parent 43235 3a8d49bc06e1
child 43299 f78d5f0818a0 
--- 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*)
isabelle