# HG changeset patch
# User wenzelm
# Date 1113410947 -7200
# Node ID 1071f41a8441a12756514aa118e69213682a8233
# Parent  f80426948b37c183add364340fd73a8f9e3204e6
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed type multi_attribute (store Attrib.src instead);
datatype elem/element(_i): Attrib.src instead of 'att;
removed map_attrib_element etc.;
added intern_attrib_elem(_expr);
added map_elem, map_values to economize code;
static binding of values in Attrib.src (cf. Args.closure, Attrib.crude_closure);
prep_facts: transfer internal facts;

diff -r f80426948b37 -r 1071f41a8441 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Apr 13 18:48:52 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 13 18:49:07 2005 +0200
@@ -2113,3 +2113,4 @@
   add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, NONE)]]];
 
 end;
+