diff -r 32f9b7a70fc0 -r be3c0df7bb90 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Fri Jul 23 09:05:54 2010 +0200
+++ b/src/HOL/Semiring_Normalization.thy	Fri Jul 23 10:25:00 2010 +0200
@@ -36,7 +36,7 @@
 
 end
 
-sublocale idom < comm_semiring_1_cancel_crossproduct
+subclass (in idom) comm_semiring_1_cancel_crossproduct
 proof
   fix w x y z
   show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"