--- 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"