adding test case for interpretation of arguments that are predicates simply as input

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 28 11:59:53 2010 +0200
@@ -1496,8 +1496,21 @@
 
 code_pred test_relation_in_output_terms .
 
-
 thm test_relation_in_output_terms.equation
 
 
+text {*
+  We want that the argument r is not treated as a higher-order relation, but simply as input.
+*}
+
+inductive test_uninterpreted_relation :: "('a => bool) => 'a list => bool"
+where
+  "list_all r xs ==> test_uninterpreted_relation r xs"
+
+code_pred (modes: i => i => bool) test_uninterpreted_relation .
+
+thm test_uninterpreted_relation.equation
+
+
+
 end