author | haftmann |
Thu, 15 May 2014 16:38:33 +0200 | |
changeset 56975 | 1f3e60572081 |
parent 56974 | 4ab498f41eee |
child 56976 | dc01225a2f77 |
--- a/src/HOL/Tools/value.ML Thu May 15 16:38:32 2014 +0200 +++ b/src/HOL/Tools/value.ML Thu May 15 16:38:33 2014 +0200 @@ -35,9 +35,6 @@ val opt_modes = Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []; -val opt_evaluator = - Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"}) - val _ = Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term" (opt_modes -- Parse.term