--- a/src/HOL/Tools/primrec_package.ML Thu May 25 15:14:20 2000 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu May 25 15:14:39 2000 +0200
@@ -102,12 +102,18 @@
handle TERM _ => raise RecError "illegal argument in pattern";
val lfrees = ls @ rs @ cargs;
+ val _ = case duplicates lfrees of
+ [] => ()
+ | vars => raise RecError("repeated variable names in pattern: " ^
+ commas_quote (map #1 vars))
+
+ val _ = case (map dest_Free (term_frees rhs)) \\ lfrees of
+ [] => ()
+ | vars => raise RecError
+ ("extra variables on rhs: " ^
+ commas_quote (map #1 vars))
in
- if not (null (duplicates 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"
- else if length middle > 1 then
+ if length middle > 1 then
raise RecError "more than one non-variable in pattern"
else (case assoc (rec_fns, fname) of
None =>