# HG changeset patch
# User wenzelm
# Date 1005261367 -3600
# Node ID 3d62ee5bec5e308c84e3de03965b3f86455ff264
# Parent  b84046fb6e027927dd37734d5f09fea99f0e4f9f
proper close_locale;

diff -r b84046fb6e02 -r 3d62ee5bec5e src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Nov 09 00:15:35 2001 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Nov 09 00:16:07 2001 +0100
@@ -69,9 +69,7 @@
 fun make_locale imports elements closed =
   {imports = imports, elements = elements, closed = closed}: locale;
 
-
-(*fun close_locale {imports, elements, closed = _} = make_locale imports elements true;*)
-fun close_locale x = x;   (* FIXME tmp *)
+fun close_locale {imports, elements, closed = _} = make_locale imports elements true;
 
 
 
@@ -86,7 +84,8 @@
 
   val empty = (NameSpace.empty, Symtab.empty);
   val copy = I;
-  fun prep_ext (space, locales) = (space, Symtab.map close_locale locales);
+  fun finish (space, locales) = (space, Symtab.map close_locale locales);
+  val prep_ext = I;
   fun merge ((space1, locales1), (space2, locales2)) =
       (NameSpace.merge (space1, space2), Symtab.merge (K true) (locales1, locales2));