diff -r aaea99edc040 -r 4044a7d1720f src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri May 09 08:13:37 2014 +0200
@@ -158,11 +158,6 @@
 
 ML_file "~~/src/HOL/Tools/value.ML"
 
-setup {*
-  Value.add_evaluator ("nbe", Nbe.dynamic_value)
-  #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
-*}
-
 
 subsection {* Generic reification *}