src/HOL/Code_Evaluation.thy
changeset 56927 4044a7d1720f
parent 56926 aaea99edc040
child 56928 1e50fddbe1f5
--- 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 *}