check if equations are present for all functions to avoid low-level exception later

--- a/src/HOL/Tools/Function/function_common.ML	Thu Nov 19 08:19:57 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Nov 19 10:33:20 2009 +0100
@@ -259,12 +259,18 @@
             (fname, length args)
           end
 
-      val _ = AList.group (op =) (map check eqs)
+      val grouped_args = AList.group (op =) (map check eqs)
+      val _ = grouped_args
         |> map (fn (fname, ars) =>
              length (distinct (op =) ars) = 1
              orelse error ("Function " ^ quote fname ^
                            " has different numbers of arguments in different equations"))
 
+      val not_defined = subtract (op =) (map fst grouped_args) fnames
+      val _ = null not_defined
+        orelse error ("No defining equations for function" ^
+          plural " " "s " not_defined ^ commas_quote not_defined)
+
       fun check_sorts ((fname, fT), _) =
           Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
           orelse error (cat_lines