# HG changeset patch
# User haftmann
# Date 1201776432 -3600
# Node ID b30a342a6e29ed60888fc1ad41f6f5b4c4d075ed
# Parent  25d06476727e6e1be5dafb54cc87f8f8ad947e4b
temporary adjustions

diff -r 25d06476727e -r b30a342a6e29 src/HOL/ex/Codegenerator_Pretty.thy
--- 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]
 
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