# HG changeset patch
# User wenzelm
# Date 1011049912 -3600
# Node ID 5f4fb54bfaf954a44fec6dfcc14ae8a6feebb94c
# Parent  f6aceb9d4b8e7ae381b1aebc9ee6262cad171adb
tuned;

diff -r f6aceb9d4b8e -r 5f4fb54bfaf9 src/Pure/Isar/isar_thy.ML
--- 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 *)