diff -r d3c7d05d8839 -r a2c4faad4d35 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Tue Jul 16 18:25:48 2002 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Tue Jul 16 18:26:09 2002 +0200
@@ -63,7 +63,7 @@
  some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z";
 
-locale semilat =
+locale (open) semilat =
   fixes A :: "'a set"
     and r :: "'a ord"
     and f :: "'a binop"