src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Oct 22 17:15:46 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Oct 22 18:38:59 2010 +0200
@@ -70,14 +70,13 @@
 where
   "False \<Longrightarrow> False''"
 
-code_pred (expected_modes: []) False'' .
+code_pred (expected_modes: bool) False'' .
 
 inductive EmptySet'' :: "'a \<Rightarrow> bool"
 where
   "False \<Longrightarrow> EmptySet'' x"
 
-code_pred (expected_modes: [1]) EmptySet'' .
-code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
+code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
 *)
 
 consts a' :: 'a