--- a/src/HOL/Finite_Set.thy Wed Oct 10 13:30:50 2012 +0200
+++ b/src/HOL/Finite_Set.thy Wed Oct 10 16:19:52 2012 +0200
@@ -1757,7 +1757,7 @@
locale folding_image_simple_idem = folding_image_simple +
assumes idem: "x * x = x"
-sublocale folding_image_simple_idem < semilattice proof
+sublocale folding_image_simple_idem < semilattice: semilattice proof
qed (fact idem)
context folding_image_simple_idem
@@ -1898,7 +1898,7 @@
locale folding_one_idem = folding_one +
assumes idem: "x * x = x"
-sublocale folding_one_idem < semilattice proof
+sublocale folding_one_idem < semilattice: semilattice proof
qed (fact idem)
context folding_one_idem