--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 06 08:11:58 2009 +0100
@@ -200,8 +200,8 @@
val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME)
-val opt_param_modes = Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum ", " opt_smode --| P.$$$ ")" >> SOME) NONE
+val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
+ P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE
val value_options =
let