# HG changeset patch
# User krauss
# Date 1227557371 -3600
# Node ID 7cef91288634cc3e44cf2ac20e6c3e0e8d792d91
# Parent  0f5b1accfb94c46d7e0e54c9928ea98c80a9b120
check for more common errors first

diff -r 0f5b1accfb94 -r 7cef91288634 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 24 21:00:03 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 24 21:09:31 2008 +0100
@@ -269,6 +269,11 @@
             fqgar
           end
           
+      val _ = mk_arities (map check eqs)
+          handle ArgumentCount fname => 
+                 error ("Function " ^ quote fname ^ 
+                        " has different numbers of arguments in different equations")
+
       fun check_sorts ((fname, fT), _) =
           Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
           orelse error (cat_lines 
@@ -276,11 +281,6 @@
            setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
 
       val _ = map check_sorts fixes
-
-      val _ = mk_arities (map check eqs)
-          handle ArgumentCount fname => 
-                 error ("Function " ^ quote fname ^ 
-                        " has different numbers of arguments in different equations")
     in
       ()
     end