Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
has_duplicates;
authorwenzelm
Tue, 07 Feb 2006 19:56:57 +0100
changeset 18973 f88976608aad
parent 18972 2905d1805e1e
child 18974 593af1a1068b
has_duplicates;
src/ZF/Tools/primrec_package.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/Tools/primrec_package.ML	Tue Feb 07 19:56:56 2006 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Tue Feb 07 19:56:57 2006 +0100
@@ -71,7 +71,7 @@
     val new_eqn = (cname, (rhs, cargs, eq))
 
   in
-    if (not o null o gen_duplicates (op =)) lfrees then
+    if has_duplicates (op =) lfrees then
       raise RecError "repeated variable name in pattern"
     else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
       raise RecError "extra variables on rhs"
isabelle