# HG changeset patch
# User wenzelm
# Date 1164560845 -3600
# Node ID 9e2ff9d4b2b0b3db1e2e58a855b1bd5820750f82
# Parent  bfe99f603933df99262a03f4ac22a588a4993ea5
Element.map_ctxt_attrib;

diff -r bfe99f603933 -r 9e2ff9d4b2b0 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Nov 26 18:07:24 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Nov 26 18:07:25 2006 +0100
@@ -935,8 +935,7 @@
         val elems = map (prep_facts ctxt) raw_elems;
         val (ctxt', res) = apsnd flat
             (activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt);
-        val elems' = elems |> map (Element.map_ctxt
-          {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
+        val elems' = elems |> map (Element.map_ctxt_attrib Args.closure);
       in (((((name, ps), mode), elems'), res), ctxt') end);
 
 in