diff -r de51a86fc903 -r cc97b347b301 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/NSA/StarDef.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -766,16 +766,16 @@
 subsection {* Ordered group classes *}
 
 instance star :: (semigroup_add) semigroup_add
-by (intro_classes, transfer, rule add_assoc)
+by (intro_classes, transfer, rule add.assoc)
 
 instance star :: (ab_semigroup_add) ab_semigroup_add
-by (intro_classes, transfer, rule add_commute)
+by (intro_classes, transfer, rule add.commute)
 
 instance star :: (semigroup_mult) semigroup_mult
-by (intro_classes, transfer, rule mult_assoc)
+by (intro_classes, transfer, rule mult.assoc)
 
 instance star :: (ab_semigroup_mult) ab_semigroup_mult
-by (intro_classes, transfer, rule mult_commute)
+by (intro_classes, transfer, rule mult.commute)
 
 instance star :: (comm_monoid_add) comm_monoid_add
 by (intro_classes, transfer, rule comm_monoid_add_class.add_0)