1.1 --- a/src/HOL/Code_Index.thy	Tue May 19 13:57:31 2009 +0200
     1.2 +++ b/src/HOL/Code_Index.thy	Tue May 19 13:57:32 2009 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Type of indices *}
     1.5  
     1.6  theory Code_Index
     1.7 -imports Main
     1.8 +imports Nat_Numeral
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -264,11 +264,6 @@
    1.13      else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
    1.14    by (auto simp add: int_of_def mod_div_equality')
    1.15  
    1.16 -lemma (in term_syntax) term_of_index_code [code]:
    1.17 -  "Code_Eval.term_of k =
    1.18 -    Code_Eval.termify (number_of :: int \<Rightarrow> int) <\<cdot>> Code_Eval.term_of_num (2::index) k"
    1.19 -  by (simp only: term_of_anything)
    1.20 -
    1.21  hide (open) const of_nat nat_of int_of
    1.22  
    1.23