explicitly check that at least one argument is present to avoid low-level exception

--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 31 15:57:10 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Apr 01 11:46:17 2009 +0200
@@ -246,6 +246,8 @@
                              ("Head symbol of left hand side must be " 
                               ^ plural "" "one out of " fnames ^ commas_quote fnames)
                                             
+            val _ = length args > 0 orelse input_error "Function has no arguments:"
+
             fun add_bvs t is = add_loose_bnos (t, 0, is)
             val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
                         |> map (fst o nth (rev qs))