--- a/src/Tools/value.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/Tools/value.ML Thu Mar 15 20:07:00 2012 +0100
@@ -57,10 +57,10 @@
in Pretty.writeln p end;
val opt_modes =
- Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
val opt_evaluator =
- Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]")
+ Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
val _ =
Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag