# HG changeset patch
# User bulwahn
# Date 1285749195 -7200
# Node ID 30c077288dfe841183309520e85c355c3e1f08e1
# Parent  05c4e9ecf5f6a1ee3227e378653bc51cb3ae5757
added test case for predicate arguments in higher-order argument position

diff -r 05c4e9ecf5f6 -r 30c077288dfe src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:15 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:15 2010 +0200
@@ -1511,6 +1511,25 @@
 
 thm test_uninterpreted_relation.equation
 
+inductive list_ex'
+where
+  "P x ==> list_ex' P (x#xs)"
+| "list_ex' P xs ==> list_ex' P (x#xs)"
+
+code_pred list_ex' .
+
+inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
+where
+  "list_ex r xs ==> test_uninterpreted_relation2 r xs"
+| "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
+
+text {* Proof procedure cannot handle this situation yet. *}
+
+code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
+
+thm test_uninterpreted_relation2.equation
+
+
 text {* Trivial predicate *}
 
 inductive implies_itself :: "'a => bool"