export in foundational order;
authorwenzelm
Sat Aug 04 22:32:41 2018 +0200 (11 months ago)
changeset 687247fafadbf16c7
parent 68723 60611540bcff
child 68725 367e60d9aa1b
export in foundational order;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sat Aug 04 16:21:25 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Aug 04 22:32:41 2018 +0200
     1.3 @@ -59,9 +59,12 @@
     1.4              else
     1.5                (case export name decl of
     1.6                  NONE => I
     1.7 -              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
     1.8 -          |> sort_by #1 |> map #2
     1.9 +              | SOME body =>
    1.10 +                  cons (#serial (Name_Space.the_entry space name),
    1.11 +                    XML.Elem (entity_markup space name, body))))
    1.12 +          |> sort (int_ord o apply2 #1) |> map #2
    1.13          end;
    1.14 +
    1.15        in if null elems then () else export_body thy export_name elems end;
    1.16  
    1.17