--- a/src/Pure/Isar/isar_thy.ML Tue Jan 15 00:11:30 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML Tue Jan 15 00:11:52 2002 +0100
@@ -695,9 +695,9 @@
(* add_locale *)
-fun add_locale (name, imports, elems) thy =
- Locale.add_locale name imports
- (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) elems) thy;
+fun add_locale (name, import, body) thy =
+ Locale.add_locale name import
+ (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body) thy;
(* theory init and exit *)