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