# HG changeset patch
# User krauss
# Date 1234702947 -3600
# Node ID 60a304bc5a07713f52bd2c01da7ced05c1c87926
# Parent  3d50e96bcd6b254981674c5671eac47224052b93
reject defined function in patterns with errmsg, e.g. f (f x) = x

diff -r 3d50e96bcd6b -r 60a304bc5a07 src/HOL/Tools/function_package/fundef_common.ML
--- 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