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)