1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Feb 06 09:05:19 2009 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Feb 06 09:05:19 2009 +0100
     1.3 @@ -124,47 +124,47 @@
     1.4  subsubsection {* Logical intermediate layer *}
     1.5  
     1.6  definition new' where
     1.7 -  [code del]: "new' = Array.new o nat_of_index"
     1.8 +  [code del]: "new' = Array.new o Code_Index.nat_of"
     1.9  hide (open) const new'
    1.10  lemma [code]:
    1.11 -  "Array.new = Array.new' o index_of_nat"
    1.12 +  "Array.new = Array.new' o Code_Index.of_nat"
    1.13    by (simp add: new'_def o_def)
    1.14  
    1.15  definition of_list' where
    1.16 -  [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
    1.17 +  [code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)"
    1.18  hide (open) const of_list'
    1.19  lemma [code]:
    1.20 -  "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
    1.21 +  "Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs"
    1.22    by (simp add: of_list'_def)
    1.23  
    1.24  definition make' where
    1.25 -  [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
    1.26 +  [code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)"
    1.27  hide (open) const make'
    1.28  lemma [code]:
    1.29 -  "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
    1.30 +  "Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)"
    1.31    by (simp add: make'_def o_def)
    1.32  
    1.33  definition length' where
    1.34 -  [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
    1.35 +  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat"
    1.36  hide (open) const length'
    1.37  lemma [code]:
    1.38 -  "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
    1.39 +  "Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of"
    1.40    by (simp add: length'_def monad_simp',
    1.41      simp add: liftM_def comp_def monad_simp,
    1.42      simp add: monad_simp')
    1.43  
    1.44  definition nth' where
    1.45 -  [code del]: "nth' a = Array.nth a o nat_of_index"
    1.46 +  [code del]: "nth' a = Array.nth a o Code_Index.nat_of"
    1.47  hide (open) const nth'
    1.48  lemma [code]:
    1.49 -  "Array.nth a n = Array.nth' a (index_of_nat n)"
    1.50 +  "Array.nth a n = Array.nth' a (Code_Index.of_nat n)"
    1.51    by (simp add: nth'_def)
    1.52  
    1.53  definition upd' where
    1.54 -  [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
    1.55 +  [code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()"
    1.56  hide (open) const upd'
    1.57  lemma [code]:
    1.58 -  "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
    1.59 +  "Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a"
    1.60    by (simp add: upd'_def monad_simp upd_return)
    1.61  
    1.62