--- a/src/HOL/Library/Code_Index.thy Wed Apr 15 15:30:39 2009 +0200
+++ b/src/HOL/Library/Code_Index.thy Wed Apr 15 15:34:00 2009 +0200
@@ -144,7 +144,7 @@
subsection {* Basic arithmetic *}
-instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
+instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
begin
definition [simp, code del]:
@@ -172,7 +172,7 @@
"n < m \<longleftrightarrow> nat_of n < nat_of m"
instance proof
-qed (auto simp add: left_distrib)
+qed (auto simp add: index left_distrib div_mult_self1)
end