--- a/src/HOL/ex/Codegenerator_Pretty.thy Thu Jan 31 11:44:46 2008 +0100
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Thu Jan 31 11:47:12 2008 +0100
@@ -9,12 +9,20 @@
imports ExecutableContent Code_Char Efficient_Nat
begin
-declare term_of_index.simps [code func del]
+setup {*
+ Code.del_funcs
+ (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "index"}))
+ #> Code.del_funcs
+ (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "char"}))
+ #> Code.del_funcs
+ (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "int"}))
+ #> Code.del_funcs
+ (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "nat"}))
+*}
declare char.recs [code func del]
char.cases [code func del]
char.size [code func del]
- term_of_char.simps [code func del]
declare isnorm.simps [code func del]
--- 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