# HG changeset patch
# User bulwahn
# Date 1285667993 -7200
# Node ID 19cb8d5581666bbaae02d199d5c2c07912c6eb61
# Parent  1cf2088cf0352fefc99a6bda699884f1e7a4a516
adding test case for interpretation of arguments that are predicates simply as input

diff -r 1cf2088cf035 -r 19cb8d558166 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- 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