| changeset 58893 | 9e0ecb66d6a7 |
| parent 58100 | f54a8a4134d3 |
| child 59323 | 468bd3aedfa1 |
--- a/src/HOL/Tools/value.ML Mon Nov 03 14:31:15 2014 +0100 +++ b/src/HOL/Tools/value.ML Mon Nov 03 14:50:27 2014 +0100 @@ -70,7 +70,7 @@ Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"}) val _ = - Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term" + Outer_Syntax.command @{command_spec "value"} "evaluate and print term" (opt_evaluator -- opt_modes -- Parse.term >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));