# HG changeset patch
# User paulson
# Date 959260479 -7200
# Node ID ac448cd4345201afd29cea0606298e0a413e8347
# Parent  b734bdb6042da3b28dff040176ae4b38aa788d38
improved error msgs, listing variable names

diff -r b734bdb6042d -r ac448cd43452 src/HOL/Tools/primrec_package.ML
--- 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 =>