src/ZF/Tools/primrec_package.ML

--- a/src/ZF/Tools/primrec_package.ML	Mon Feb 06 11:00:24 2006 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Mon Feb 06 11:01:28 2006 +0100
@@ -71,7 +71,7 @@
     val new_eqn = (cname, (rhs, cargs, eq))
 
   in
-    if not (null (duplicates lfrees)) then
+    if (not o null o gen_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"