src/HOL/Code_Index.thy

--- a/src/HOL/Code_Index.thy	Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/Code_Index.thy	Tue May 19 13:57:32 2009 +0200
@@ -3,7 +3,7 @@
 header {* Type of indices *}
 
 theory Code_Index
-imports Main
+imports Nat_Numeral
 begin
 
 text {*
@@ -264,11 +264,6 @@
     else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   by (auto simp add: int_of_def mod_div_equality')
 
-lemma (in term_syntax) term_of_index_code [code]:
-  "Code_Eval.term_of k =
-    Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k"
-  by (simp only: term_of_anything)
-
 hide (open) const of_nat nat_of int_of