adopted mode syntax for values command
authorbulwahn
Fri, 06 Nov 2009 08:11:58 +0100
changeset 33481 030db03cb426
parent 33480 dcfe9100e0a6
child 33482 5029ec373036
adopted mode syntax for values command
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- 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