Element.map_ctxt_attrib;
authorwenzelm
Sun, 26 Nov 2006 18:07:25 +0100
changeset 21530 9e2ff9d4b2b0
parent 21529 bfe99f603933
child 21531 43aa65a8a870
Element.map_ctxt_attrib;
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