export in foundational order;
authorwenzelm
Sat, 04 Aug 2018 22:32:41 +0200
changeset 68724 7fafadbf16c7
parent 68723 60611540bcff
child 68725 367e60d9aa1b
export in foundational order;
src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Aug 04 16:21:25 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Aug 04 22:32:41 2018 +0200
@@ -59,9 +59,12 @@
             else
               (case export name decl of
                 NONE => I
-              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
-          |> sort_by #1 |> map #2
+              | SOME body =>
+                  cons (#serial (Name_Space.the_entry space name),
+                    XML.Elem (entity_markup space name, body))))
+          |> sort (int_ord o apply2 #1) |> map #2
         end;
+
       in if null elems then () else export_body thy export_name elems end;