
diff -r d716eb002b9f -r db2953f5887a src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 28 16:45:50 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 28 16:45:51 2010 +0200
@@ -686,6 +686,13 @@
 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
 
+subsection {* Free function variable *}
+
+inductive FF :: "nat => nat => bool"
+where
+  "f x = y ==> FF x y"
+
+code_pred FF .
 
 subsection {* IMP *}
 




