# HG changeset patch
# User haftmann
# Date 1400164713 -7200
# Node ID 1f3e6057208151cd4fc1abe17adcdb8a2994b5b0
# Parent  4ab498f41eee1e5d3682199b2d20923305fd1e03
dropped dead code

diff -r 4ab498f41eee -r 1f3e60572081 src/HOL/Tools/value.ML
--- 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