# 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;