# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 030db03cb42668ec2e33286d116c81bf50676e9d
# Parent  dcfe9100e0a63e7c1b00b48d453e4e8bafa650d7
adopted mode syntax for values command

diff -r dcfe9100e0a6 -r 030db03cb426 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