diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Lattices_Big.thy	Fri Dec 27 14:35:14 2013 +0100
@@ -308,15 +308,14 @@
 
 subsection {* Lattice operations on finite sets *}
 
-definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
+context semilattice_inf
+begin
+
+definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
 where
   "Inf_fin = semilattice_set.F inf"
 
-definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
-where
-  "Sup_fin = semilattice_set.F sup"
-
-sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
+sublocale Inf_fin!: semilattice_order_set inf less_eq less
 where
   "semilattice_set.F inf = Inf_fin"
 proof -
@@ -325,7 +324,16 @@
   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
 qed
 
-sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
+end
+
+context semilattice_sup
+begin
+
+definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
+where
+  "Sup_fin = semilattice_set.F sup"
+
+sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
 where
   "semilattice_set.F sup = Sup_fin"
 proof -
@@ -334,13 +342,11 @@
   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
 qed
 
+end
+
 
 subsection {* Infimum and Supremum over non-empty sets *}
 
-text {*
-  After this non-regular bootstrap, things continue canonically.
-*}
-
 context lattice
 begin
 
@@ -449,7 +455,7 @@
 
 lemma Inf_fin_Inf:
   assumes "finite A" and "A \<noteq> {}"
-  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
+  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
 proof -
   from assms obtain b B where "A = insert b B" and "finite B" by auto
   then show ?thesis
@@ -458,7 +464,7 @@
 
 lemma Sup_fin_Sup:
   assumes "finite A" and "A \<noteq> {}"
-  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
+  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
 proof -
   from assms obtain b B where "A = insert b B" and "finite B" by auto
   then show ?thesis