--- a/src/HOL/NSA/StarDef.thy Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy Fri Oct 19 15:12:52 2012 +0200
@@ -828,8 +828,8 @@
instance star :: (semiring) semiring
apply (intro_classes)
-apply (transfer, rule left_distrib)
-apply (transfer, rule right_distrib)
+apply (transfer, rule distrib_right)
+apply (transfer, rule distrib_left)
done
instance star :: (semiring_0) semiring_0
@@ -838,7 +838,7 @@
instance star :: (semiring_0_cancel) semiring_0_cancel ..
instance star :: (comm_semiring) comm_semiring
-by (intro_classes, transfer, rule left_distrib)
+by (intro_classes, transfer, rule distrib_right)
instance star :: (comm_semiring_0) comm_semiring_0 ..
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..