diff -r d8549f4d900b -r 791607529f6d src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Tue Jun 10 15:30:06 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy	Tue Jun 10 15:30:33 2008 +0200
@@ -10,7 +10,7 @@
 
 text {*
   Indices are isomorphic to HOL @{typ nat} but
-  mapped to target-language builtin integers
+  mapped to target-language builtin integers.
 *}
 
 subsection {* Datatype of indices *}
@@ -74,35 +74,23 @@
 definition [simp]:
   "Suc_index k = index_of_nat (Suc (nat_of_index k))"
 
-lemma index_induct: "P 0 \<Longrightarrow> (\<And>k. P k \<Longrightarrow> P (Suc_index k)) \<Longrightarrow> P k"
+rep_datatype "0 \<Colon> index" Suc_index
 proof -
+  fix P :: "index \<Rightarrow> bool"
+  fix k :: index
   assume "P 0" then have init: "P (index_of_nat 0)" by simp
   assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
-    then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat (n)))" .
+    then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" .
     then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp
   from init step have "P (index_of_nat (nat_of_index k))"
     by (induct "nat_of_index k") simp_all
   then show "P k" by simp
-qed
-
-lemma Suc_not_Zero_index: "Suc_index k \<noteq> 0"
-  by simp
-
-lemma Zero_not_Suc_index: "0 \<noteq> Suc_index k"
-  by simp
-
-lemma Suc_Suc_index_eq: "Suc_index k = Suc_index l \<longleftrightarrow> k = l"
-  by simp
-
-rep_datatype index
-  distinct  Suc_not_Zero_index Zero_not_Suc_index
-  inject    Suc_Suc_index_eq
-  induction index_induct
+qed simp_all
 
 lemmas [code func del] = index.recs index.cases
 
 declare index_case [case_names nat, cases type: index]
-declare index_induct [case_names nat, induct type: index]
+declare index.induct [case_names nat, induct type: index]
 
 lemma [code func]:
   "index_size = nat_of_index"