1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Apr 20 12:27:23 2009 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Apr 21 09:53:24 2009 +0200
     1.3 @@ -215,21 +215,6 @@
     1.4        (fname, qs, gs, args, rhs)
     1.5      end
     1.6  
     1.7 -exception ArgumentCount of string
     1.8 -
     1.9 -fun mk_arities fqgars =
    1.10 -    let fun f (fname, _, _, args, _) arities =
    1.11 -            let val k = length args
    1.12 -            in
    1.13 -              case Symtab.lookup arities fname of
    1.14 -                NONE => Symtab.update (fname, k) arities
    1.15 -              | SOME i => (if i = k then arities else raise ArgumentCount fname)
    1.16 -            end
    1.17 -    in
    1.18 -      fold f fqgars Symtab.empty
    1.19 -    end
    1.20 -
    1.21 -
    1.22  (* Check for all sorts of errors in the input *)
    1.23  fun check_defs ctxt fixes eqs =
    1.24      let
    1.25 @@ -269,13 +254,14 @@
    1.26                       " occur" ^ plural "s" "" funvars ^ " in function position.",  
    1.27                       "Misspelled constructor???"]); true)
    1.28            in
    1.29 -            fqgar
    1.30 +            (fname, length args)
    1.31            end
    1.32 -          
    1.33 -      val _ = mk_arities (map check eqs)
    1.34 -          handle ArgumentCount fname => 
    1.35 -                 error ("Function " ^ quote fname ^ 
    1.36 -                        " has different numbers of arguments in different equations")
    1.37 +
    1.38 +      val _ = AList.group (op =) (map check eqs)
    1.39 +        |> map (fn (fname, ars) =>
    1.40 +             length (distinct (op =) ars) = 1
    1.41 +             orelse error ("Function " ^ quote fname ^
    1.42 +                           " has different numbers of arguments in different equations"))
    1.43  
    1.44        fun check_sorts ((fname, fT), _) =
    1.45            Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)

     2.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Apr 20 12:27:23 2009 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Apr 21 09:53:24 2009 +0200
     2.3 @@ -215,11 +215,11 @@
     2.4      #> Proof.global_future_terminal_proof
     2.5        (Method.Basic (method, Position.none), NONE) int
     2.6  
     2.7 -fun mk_catchall fixes arities =
     2.8 +fun mk_catchall fixes arity_of =
     2.9      let
    2.10        fun mk_eqn ((fname, fT), _) =
    2.11            let 
    2.12 -            val n = the (Symtab.lookup arities fname)
    2.13 +            val n = arity_of fname
    2.14              val (argTs, rT) = chop n (binder_types fT)
    2.15                                     |> apsnd (fn Ts => Ts ---> body_type fT) 
    2.16                                
    2.17 @@ -235,7 +235,12 @@
    2.18      end
    2.19  
    2.20  fun add_catchall ctxt fixes spec =
    2.21 -    spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec))
    2.22 +  let val fqgars = map (split_def ctxt) spec
    2.23 +      val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
    2.24 +                     |> AList.lookup (op =) #> the
    2.25 +  in
    2.26 +    spec @ mk_catchall fixes arity_of
    2.27 +  end
    2.28  
    2.29  fun warn_if_redundant ctxt origs tss =
    2.30      let

     3.1 --- a/src/HOL/Tools/function_package/mutual.ML	Mon Apr 20 12:27:23 2009 +0200
     3.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Apr 21 09:53:24 2009 +0200
     3.3 @@ -87,12 +87,12 @@
     3.4        val num = length fs
     3.5          val fnames = map fst fs
     3.6          val fqgars = map (split_def ctxt) eqs
     3.7 -        val arities = mk_arities fqgars
     3.8 +        val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
     3.9 +                       |> AList.lookup (op =) #> the
    3.10  
    3.11          fun curried_types (fname, fT) =
    3.12              let
    3.13 -              val k = the_default 1 (Symtab.lookup arities fname)
    3.14 -              val (caTs, uaTs) = chop k (binder_types fT)
    3.15 +              val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
    3.16              in
    3.17                  (caTs, uaTs ---> body_type fT)
    3.18              end