# HG changeset patch
# User berghofe
# Date 1008151662 -3600
# Node ID 0404454d97df0b4dbd8568437b2d7ce078e31bf5
# Parent  f41e477576b901b543f05d3a9f1baba6a0a74a85
Improved error messages.

diff -r f41e477576b9 -r 0404454d97df src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Dec 12 09:04:20 2001 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Dec 12 11:07:42 2001 +0100
@@ -64,20 +64,16 @@
       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))
+    fun check_vars _ [] = ()
+      | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
   in
     if length middle > 1 then 
       raise RecError "more than one non-variable in pattern"
-    else (case assoc (rec_fns, fname) of
+    else
+     (check_vars "repeated variable names in pattern: " (duplicates lfrees);
+      check_vars "extra variables on rhs: "
+        (map dest_Free (term_frees rhs) \\ lfrees);
+      case assoc (rec_fns, fname) of
         None =>
           (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
       | Some (_, rpos', eqns) =>