diff -r 7ebe8dc06cbb -r 4f06fae6a55e src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Tue Sep 16 09:21:24 2008 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Tue Sep 16 09:21:26 2008 +0200
@@ -11,7 +11,6 @@
   Binomial
   Commutative_Ring
   Enum
-  Eval
   List_Prefix
   Nat_Infinity
   Nested_Environment
@@ -20,19 +19,10 @@
   Primes
   Product_ord
   SetsAndFunctions
-  State_Monad
   While_Combinator
   Word
   "~~/src/HOL/ex/Commutative_Ring_Complete"
   "~~/src/HOL/ex/Records"
 begin
 
-lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
-declare fast_bv_to_nat_helper.simps [code func del]
-
-setup {*
-  Code.del_funcs
-    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "env"}))
-*}
-
 end