# HG changeset patch
# User wenzelm
# Date 1533414761 -7200
# Node ID 7fafadbf16c7fe6b958230fa03217e80c56f0cd8
# Parent  60611540bcffe33dcba974674bcd801f653a3f73
export in foundational order;

diff -r 60611540bcff -r 7fafadbf16c7 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;