diff -r 54db9b5080b8 -r 4134f7c782e2 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Nov 30 20:13:05 2007 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Nov 30 20:13:06 2007 +0100
@@ -471,7 +471,7 @@
 begin
 
 subclass pordered_cancel_ab_semigroup_add
-  by unfold_locales
+  by intro_locales
 
 subclass pordered_ab_semigroup_add_imp_le
 proof unfold_locales
@@ -483,7 +483,7 @@
 qed
 
 subclass pordered_comm_monoid_add
-  by unfold_locales
+  by intro_locales
 
 lemma max_diff_distrib_left:
   shows "max x y - z = max (x - z) (y - z)"
@@ -629,7 +629,7 @@
 begin
 
 subclass ordered_ab_semigroup_add
-  by unfold_locales
+  by intro_locales
 
 subclass pordered_ab_semigroup_add_imp_le
 proof unfold_locales
@@ -657,7 +657,7 @@
 begin
 
 subclass ordered_cancel_ab_semigroup_add 
-  by unfold_locales
+  by intro_locales
 
 lemma neg_less_eq_nonneg:
   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
@@ -946,8 +946,8 @@
 class lordered_ab_group_add = pordered_ab_group_add + lattice
 begin
 
-subclass lordered_ab_group_add_meet by unfold_locales
-subclass lordered_ab_group_add_join by unfold_locales
+subclass lordered_ab_group_add_meet by intro_locales
+subclass lordered_ab_group_add_join by intro_locales
 
 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left