| changeset 59936 | b8ffc3dc9e24 |
| parent 59323 | 468bd3aedfa1 |
| child 62969 | 9f394a16c557 |
--- a/src/HOL/Tools/value.ML Mon Apr 06 16:30:44 2015 +0200 +++ b/src/HOL/Tools/value.ML Mon Apr 06 17:06:48 2015 +0200 @@ -70,7 +70,7 @@ Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"}) val _ = - Outer_Syntax.command @{command_spec "value"} "evaluate and print term" + Outer_Syntax.command @{command_keyword value} "evaluate and print term" (opt_evaluator -- opt_modes -- Parse.term >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));