diff -r 832b9269dedd -r cb87f103d114 src/HOL/ex/LocaleGroup.ML
--- a/src/HOL/ex/LocaleGroup.ML	Fri Dec 11 10:38:51 1998 +0100
+++ b/src/HOL/ex/LocaleGroup.ML	Fri Dec 11 10:41:53 1998 +0100
@@ -139,7 +139,7 @@
 by (asm_simp_tac (simpset() addsimps [binop_assoc]) 1);
 qed "right_cancellation";
 
-Close_locale();
+Close_locale "groups";
 
 (* example what happens if export *)
 val Left_cancellation = export left_cancellation;