--- 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));