Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Wed, 01 Apr 2009 11:53:59 +0200
changeset 30833 0e6ee93d0fa2
parent 30832 521f7d801da1 (diff)
parent 30831 7c6e1843fda5 (current diff)
child 30835 46e16145d4bd
merged
--- 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))
isabelle