# HG changeset patch
# User wenzelm
# Date 1238579639 -7200
# Node ID 0e6ee93d0fa23917e496d9a792c23af23924f29a
# Parent  521f7d801da1d4bb49fc9b1882e30bed7771d635# Parent  7c6e1843fda57975a4c57386b9dd4da030c65a18
merged

diff -r 7c6e1843fda5 -r 0e6ee93d0fa2 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Apr 01 11:46:56 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Apr 01 11:53:59 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))