# HG changeset patch
# User paulson
# Date 913369313 -3600
# Node ID cb87f103d114b5fb3166d5f08af2f9f25de5a2aa
# Parent  832b9269dedd0f1868748123cb097fb46e8eb1ac
new Close_locale synatx

diff -r 832b9269dedd -r cb87f103d114 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];
diff -r 832b9269dedd -r cb87f103d114 src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:38:51 1998 +0100
+++ b/src/HOL/Induct/Multiset.ML	Fri Dec 11 10:41:53 1998 +0100
@@ -431,7 +431,7 @@
 by(blast_tac (claset() addDs [export lemma3]) 1);
 qed "all_accessible";
 
-Close_locale();
+Close_locale "MSOrd";
 
 Goal "wf(r) ==> wf(mult1 r)";
 by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
diff -r 832b9269dedd -r cb87f103d114 src/HOL/Real/Hyperreal/Filter.ML
--- a/src/HOL/Real/Hyperreal/Filter.ML	Fri Dec 11 10:38:51 1998 +0100
+++ b/src/HOL/Real/Hyperreal/Filter.ML	Fri Dec 11 10:41:53 1998 +0100
@@ -552,6 +552,6 @@
 
 val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
 
-Close_locale();
+Close_locale "UFT";
 
 
diff -r 832b9269dedd -r cb87f103d114 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Fri Dec 11 10:38:51 1998 +0100
+++ b/src/HOL/UNITY/Lift.ML	Fri Dec 11 10:41:53 1998 +0100
@@ -435,4 +435,4 @@
 by (Blast_tac 1);
 qed "lift_1";
 
-Close_locale();
+Close_locale "floor";
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;