src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Aug 03 11:09:12 2011 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 03 13:59:59 2011 +0200
@@ -1962,10 +1962,6 @@
 
 subsubsection {* Evaluation and normalization by evaluation *}
 
-setup {*
-  Value.add_evaluator ("SML", Codegen.eval_term)
-*}
-
 ML {*
 fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   (CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 (conv ctxt))) ctxt)