dropped dead code
authorhaftmann
Thu May 15 16:38:33 2014 +0200 (2014-05-15)
changeset 569751f3e60572081
parent 56974 4ab498f41eee
child 56976 dc01225a2f77
dropped dead code
src/HOL/Tools/value.ML
     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