src/HOL/Finite.ML

--- a/src/HOL/Finite.ML	Fri Dec 11 10:38:51 1998 +0100
+++ b/src/HOL/Finite.ML	Fri Dec 11 10:41:53 1998 +0100
@@ -675,7 +675,7 @@
 Delrules [empty_foldSetE];
 Delrules foldSet.intrs;
 
-Close_locale();
+Close_locale "LC";
 
 Open_locale "ACe"; 
 
@@ -722,7 +722,7 @@
            [export fold_insert,insert_absorb, Int_insert_left]) 1);
 qed "fold_Un_disjoint2";
 
-Close_locale();
+Close_locale "ACe";
 
 Delrules ([empty_foldSetE] @ foldSet.intrs);
 Delsimps [foldSet_imp_finite];