diff -r 25d06476727e -r b30a342a6e29 src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Thu Jan 31 11:44:46 2008 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Thu Jan 31 11:47:12 2008 +0100
@@ -9,7 +9,7 @@
   Main
   Eval
   Code_Index
-  "~~/src/HOL/ex/Records"
+  (*"~~/src/HOL/ex/Records"*)
   AssocList
   Binomial
   Commutative_Ring
@@ -29,7 +29,7 @@
   Word
 begin
 
-declare term_of_index.simps [code func del]
+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]
 
 end