src/HOL/ex/Locales.thy

     have "prod (semigroup_product ?G' ?H') = prod I"
       by (simp add: I_def group_product_def group.defs
 	semigroup_product_def semigroup.defs)
     moreover
     have "semigroup ?G'" and "semigroup ?H'"
-      using prems by (simp_all add: semigroup_def semigroup.defs)
+      using prems by (simp_all add: semigroup_def semigroup.defs G.assoc H.assoc)
     then have "semigroup (semigroup_product ?G' ?H')" ..
     ultimately show ?thesis by (simp add: I_def semigroup_def)
   qed
   show "group_axioms I"
   proof