src/HOL/Code_Eval.thy

 *)
 
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Eval
-imports Plain Typerep
+imports Plain Typerep Code_Index
 begin
 
 subsection {* Term representation *}
 
 subsubsection {* Terms and class @{text term_of} *}

   "term_of (k::int) = (if k = 0 then termify (0 :: int)
     else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k
       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 *}
 
 print_translation {*
 let