diff -r 74f6817870f9 -r dd602eb20f3f src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Fri Jan 25 14:54:44 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Fri Jan 25 14:54:46 2008 +0100
@@ -17,6 +17,10 @@
 
 datatype index = index_of_nat nat
 
+lemma [code func]:
+  "index_size k = 0"
+  by (cases k) simp
+
 lemmas [code func del] = index.recs index.cases
 
 primrec
@@ -76,6 +80,8 @@
 lemma zero_index_code [code inline, code func]:
   "(0\<Colon>index) = Numeral0"
   by (simp add: number_of_index_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>index)"
+  using zero_index_code ..
 
 definition [simp, code func del]:
   "(1\<Colon>index) = index_of_nat 1"
@@ -83,6 +89,8 @@
 lemma one_index_code [code inline, code func]:
   "(1\<Colon>index) = Numeral1"
   by (simp add: number_of_index_def Pls_def Bit_def)
+lemma [code post]: "Numeral1 = (1\<Colon>index)"
+  using one_index_code ..
 
 definition [simp, code func del]:
   "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
@@ -179,7 +187,7 @@
 code_type index
   (SML "int")
   (OCaml "int")
-  (Haskell "Integer")
+  (Haskell "Int")
 
 code_instance index :: eq
   (Haskell -)
@@ -194,7 +202,7 @@
 
 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   (SML "Int.+/ ((_),/ (_))")
-  (OCaml "Pervasives.(+)")
+  (OCaml "Pervasives.( + )")
   (Haskell infixl 6 "+")
 
 code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
@@ -204,12 +212,12 @@
 
 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   (SML "Int.*/ ((_),/ (_))")
-  (OCaml "Pervasives.(*)")
+  (OCaml "Pervasives.( * )")
   (Haskell infixl 7 "*")
 
 code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
   (SML "Int.div/ ((_),/ (_))")
-  (OCaml "Pervasives.(/)")
+  (OCaml "Pervasives.( / )")
   (Haskell "div")
 
 code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
@@ -219,17 +227,17 @@
 
 code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
-  (OCaml "!((_ : Pervasives.int) = _)")
+  (OCaml "!((_ : int) = _)")
   (Haskell infixl 4 "==")
 
 code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   (SML "Int.<=/ ((_),/ (_))")
-  (OCaml "!((_ : Pervasives.int) <= _)")
+  (OCaml "!((_ : int) <= _)")
   (Haskell infix 4 "<=")
 
 code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
-  (OCaml "!((_ : Pervasives.int) < _)")
+  (OCaml "!((_ : int) < _)")
   (Haskell infix 4 "<")
 
 end