src/HOL/Tools/value.ML
changeset 56975 1f3e60572081
parent 56927 4044a7d1720f
child 58100 f54a8a4134d3
     1.1 --- a/src/HOL/Tools/value.ML	Thu May 15 16:38:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/value.ML	Thu May 15 16:38:33 2014 +0200
     1.3 @@ -35,9 +35,6 @@
     1.4  val opt_modes =
     1.5    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
     1.6  
     1.7 -val opt_evaluator =
     1.8 -  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
     1.9 -  
    1.10  val _ =
    1.11    Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    1.12      (opt_modes -- Parse.term