--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Aug 23 15:30:42 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Aug 23 16:47:55 2010 +0200
@@ -348,6 +348,9 @@
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 .
@@ -409,6 +412,10 @@
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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Aug 23 16:47:55 2010 +0200
@@ -200,10 +200,10 @@
(Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
and parse_mode_tuple_expr xs =
- (parse_mode_basic_expr --| Args.$$$ "*" -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
+ (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
xs
and parse_mode_expr xs =
- (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
+ (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE