diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -6,7 +6,9 @@
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
 
-theory Group imports FuncSet Lattice begin
+theory Group
+imports Lattice FuncSet
+begin
 
 
 section {* Monoids and Groups *}
@@ -280,7 +282,7 @@
   qed
   then have carrier_subset_Units: "carrier G <= Units G"
     by (unfold Units_def) fast
-  show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
+  show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
 qed
 
 lemma (in monoid) group_l_invI:
@@ -685,7 +687,7 @@
   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
       x \<otimes> y = y \<otimes> x"
   shows "comm_group G"
-  by unfold_locales (simp_all add: m_comm)
+  proof qed (simp_all add: m_comm)
 
 lemma comm_groupI:
   fixes G (structure)
@@ -713,7 +715,7 @@
 
 theorem (in group) subgroups_partial_order:
   "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
-  by unfold_locales simp_all
+  proof qed simp_all
 
 lemma (in group) subgroup_self:
   "subgroup (carrier G) G"