diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Tue May 19 13:57:32 2009 +0200
@@ -5,7 +5,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Eval
-imports Plain Typerep
+imports Plain Typerep Code_Index
 begin
 
 subsection {* Term representation *}
@@ -215,6 +215,9 @@
       else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))"
   by (simp only: term_of_anything)
 
+lemma (in term_syntax) term_of_index_code [code]:
+  "term_of (k::index) = termify (number_of :: int \<Rightarrow> index) <\<cdot>> term_of_num (2::index) k"
+  by (simp only: term_of_anything)
 
 subsection {* Obfuscate *}