# HG changeset patch
# User krauss
# Date 1238579177 -7200
# Node ID 521f7d801da1d4bb49fc9b1882e30bed7771d635
# Parent  d64a293f23ba8a923ef4d47450ab7258d0960d9d
explicitly check that at least one argument is present to avoid low-level exception

diff -r d64a293f23ba -r 521f7d801da1 src/HOL/Tools/function_package/fundef_common.ML
--- 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))