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/Import/hol4rews.ML
changeset 36692 54b64d4ad524
parent 35250 92664dca6f20
child 38551 8ddfc68a3908 
--- a/src/HOL/Import/hol4rews.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML	Wed May 05 18:25:34 2010 +0200
@@ -604,9 +604,9 @@
                 val defname = Thm.def_name name
                 val pdefname = name ^ "_primdef"
             in
-                if not (defname mem used)
+                if not (member (op =) used defname)
                 then F defname                 (* name_def *)
-                else if not (pdefname mem used)
+                else if not (member (op =) used pdefname)
                 then F pdefname                (* name_primdef *)
                 else F (Name.variant used pdefname) (* last resort *)
             end
isabelle