1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Oct 22 17:15:46 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Oct 22 18:38:59 2010 +0200
     1.3 @@ -70,14 +70,13 @@
     1.4  where
     1.5    "False \<Longrightarrow> False''"
     1.6  
     1.7 -code_pred (expected_modes: []) False'' .
     1.8 +code_pred (expected_modes: bool) False'' .
     1.9  
    1.10  inductive EmptySet'' :: "'a \<Rightarrow> bool"
    1.11  where
    1.12    "False \<Longrightarrow> EmptySet'' x"
    1.13  
    1.14 -code_pred (expected_modes: [1]) EmptySet'' .
    1.15 -code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
    1.16 +code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
    1.17  *)
    1.18  
    1.19  consts a' :: 'a