src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy

     "append [] xs xs"
   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
 code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix,
   i => o => i => bool as suffix, i => i => i => bool) append .
+code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as "concat", o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as "slice", o \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool as prefix,
+  i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool as suffix, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) append .
+
 code_pred [dseq] append .
 code_pred [random_dseq] append .
 
 thm append.equation
 thm append.dseq_equation

   "tupled_append ([], xs, xs)"
 | "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
 
 code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool,
   i * o * i => bool, i * i * i => bool) tupled_append .
+
+code_pred (expected_modes: i \<times> i \<times> o \<Rightarrow> bool, o \<times> o \<times> i \<Rightarrow> bool, o \<times> i \<times> i \<Rightarrow> bool,
+  i \<times> o \<times> i \<Rightarrow> bool, i \<times> i \<times> i \<Rightarrow> bool) tupled_append .
+
 code_pred [random_dseq] tupled_append .
 thm tupled_append.equation
 
 values "{xs. tupled_append ([(1::nat), 2, 3], [4, 5], xs)}"