src/ZF/AC/AC16_WO4.thy

--- a/src/ZF/AC/AC16_WO4.thy	Tue Jul 16 18:46:13 2002 +0200
+++ b/src/ZF/AC/AC16_WO4.thy	Tue Jul 16 18:46:59 2002 +0200
@@ -203,7 +203,7 @@
                  succ_lepoll_natE)
 
 
-locale AC16 =
+locale (open) AC16 =
   fixes x and y and k and l and m and t_n and R and MM and LL and GG and s 
   defines k_def:     "k   == succ(l)"
       and MM_def:    "MM  == {v \<in> t_n. succ(k) \<lesssim> v Int y}"