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 43301 8d7fc4a5b502
parent 43299 f78d5f0818a0
child 43303 c4ea897a5326 
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Jun 09 00:16:28 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 (metis_aconv_untyped o pairself prop_of) ths1)
+  exists (member (Term.aconv_untyped o pairself prop_of) ths1)
          (map Meson.make_meta_clause ths2)
 
 (*Determining which axiom clauses are actually used*)
isabelle