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.
reject defined function in patterns with errmsg, e.g. f (f x) = x
authorkrauss
Sun, 15 Feb 2009 14:02:27 +0100
changeset 29922 60a304bc5a07
parent 29921 3d50e96bcd6b
child 29924 f270fe271a65
reject defined function in patterns with errmsg, e.g. f (f x) = x
src/HOL/Tools/function_package/fundef_common.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/fundef_common.ML	Sun Feb 15 11:34:46 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sun Feb 15 14:02:27 2009 +0100
@@ -254,8 +254,8 @@
                          ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
                                     
             val _ = forall (not o Term.exists_subterm 
-                             (fn Free (n, _) => n mem fnames | _ => false)) gs 
-                    orelse input_error "Recursive Calls not allowed in premises"
+                             (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
+                    orelse input_error "Defined function may not occur in premises or arguments"
 
             val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
             val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
isabelle