
diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Mon Mar 17 18:37:05 2008 +0100
@@ -45,7 +45,7 @@
   shows P
   by (rule assms [of "nat_of_index k"]) simp
 
-lemma index_induct:
+lemma index_induct_raw:
   assumes "\<And>n. P (index_of_nat n)"
   shows "P k"
 proof -




