# HG changeset patch
# User bulwahn
# Date 1258624183 -3600
# Node ID bc75dbbbf3e6c5dbc4d70502bbac69469daa0798
# Parent  47b7c9e0bf6e62b89b6e3b282d36924195905a27# Parent  7ead0ccf6cbd35437ea43032a613601be2ee431f
merged

diff -r 47b7c9e0bf6e -r bc75dbbbf3e6 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Thu Nov 19 08:25:57 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Nov 19 10:49:43 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