--- a/src/HOL/Finite_Set.thy Wed Oct 10 15:27:10 2012 +0200
+++ b/src/HOL/Finite_Set.thy Wed Oct 10 15:39:01 2012 +0200
@@ -1771,7 +1771,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
@@ -1912,7 +1912,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