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