# HG changeset patch
# User wenzelm
# Date 1139338617 -3600
# Node ID f88976608aad249ac3904521a3fb7df126ca4e27
# Parent  2905d1805e1e32076d05c3dde0250a9cd5ff9b71
has_duplicates;

diff -r 2905d1805e1e -r f88976608aad src/ZF/Tools/primrec_package.ML
--- 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"