--- 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 *}