Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/fundef_common.ML
changeset 30832 521f7d801da1
parent 30791 02aa92682e88
child 30906 3c7a76e79898 
--- 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))
isabelle