src/HOL/Algebra/AbelCoset.thy

 proof -
   interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
   by (rule a_normal)
 
   show "abelian_subgroup H G"
-  by (unfold_locales, simp add: a_comm)
+  proof qed (simp add: a_comm)
 qed
 
 lemma abelian_subgroupI2:
   fixes G (structure)
   assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"

     done
 qed
 
 lemma (in abelian_group_hom) is_abelian_group_hom:
   "abelian_group_hom G H h"
-by (unfold_locales)
+  ..
 
 lemma (in abelian_group_hom) hom_add [simp]:
   "[| x : carrier G; y : carrier G |]
         ==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
 by (rule group_hom.hom_mult[OF a_group_hom,