# HG changeset patch
# User krauss
# Date 1240300404 -7200
# Node ID 3c7a76e79898668855d22d8d39e444b7bd0bcade
# Parent  e3bbc2c4c58147226bf6360423b0b3cd60179cae
simplify computation and consistency checks of argument counts in the input

diff -r e3bbc2c4c581 -r 3c7a76e79898 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Apr 21 09:53:24 2009 +0200
@@ -215,21 +215,6 @@
       (fname, qs, gs, args, rhs)
     end
 
-exception ArgumentCount of string
-
-fun mk_arities fqgars =
-    let fun f (fname, _, _, args, _) arities =
-            let val k = length args
-            in
-              case Symtab.lookup arities fname of
-                NONE => Symtab.update (fname, k) arities
-              | SOME i => (if i = k then arities else raise ArgumentCount fname)
-            end
-    in
-      fold f fqgars Symtab.empty
-    end
-
-
 (* Check for all sorts of errors in the input *)
 fun check_defs ctxt fixes eqs =
     let
@@ -269,13 +254,14 @@
                      " occur" ^ plural "s" "" funvars ^ " in function position.",  
                      "Misspelled constructor???"]); true)
           in
-            fqgar
+            (fname, length args)
           end
-          
-      val _ = mk_arities (map check eqs)
-          handle ArgumentCount fname => 
-                 error ("Function " ^ quote fname ^ 
-                        " has different numbers of arguments in different equations")
+
+      val _ = AList.group (op =) (map check eqs)
+        |> map (fn (fname, ars) =>
+             length (distinct (op =) ars) = 1
+             orelse 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)
diff -r e3bbc2c4c581 -r 3c7a76e79898 src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Apr 21 09:53:24 2009 +0200
@@ -215,11 +215,11 @@
     #> Proof.global_future_terminal_proof
       (Method.Basic (method, Position.none), NONE) int
 
-fun mk_catchall fixes arities =
+fun mk_catchall fixes arity_of =
     let
       fun mk_eqn ((fname, fT), _) =
           let 
-            val n = the (Symtab.lookup arities fname)
+            val n = arity_of fname
             val (argTs, rT) = chop n (binder_types fT)
                                    |> apsnd (fn Ts => Ts ---> body_type fT) 
                               
@@ -235,7 +235,12 @@
     end
 
 fun add_catchall ctxt fixes spec =
-    spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec))
+  let val fqgars = map (split_def ctxt) spec
+      val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
+                     |> AList.lookup (op =) #> the
+  in
+    spec @ mk_catchall fixes arity_of
+  end
 
 fun warn_if_redundant ctxt origs tss =
     let
diff -r e3bbc2c4c581 -r 3c7a76e79898 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Apr 21 09:53:24 2009 +0200
@@ -87,12 +87,12 @@
       val num = length fs
         val fnames = map fst fs
         val fqgars = map (split_def ctxt) eqs
-        val arities = mk_arities fqgars
+        val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
+                       |> AList.lookup (op =) #> the
 
         fun curried_types (fname, fT) =
             let
-              val k = the_default 1 (Symtab.lookup arities fname)
-              val (caTs, uaTs) = chop k (binder_types fT)
+              val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
             in
                 (caTs, uaTs ---> body_type fT)
             end