--- 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