diff -r 4e4738698db4 -r 9f394a16c557 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Tools/value.ML	Wed Apr 13 18:01:05 2016 +0200
@@ -64,10 +64,10 @@
   in Pretty.writeln p end;
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
 
 val opt_evaluator =
-  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
+  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
   
 val _ =
   Outer_Syntax.command @{command_keyword value} "evaluate and print term"