src/Pure/Thy/export_theory.ML
changeset 68724 7fafadbf16c7
parent 68539 6740e3611a86
child 68725 367e60d9aa1b
equal deleted inserted replaced
68723:60611540bcff 68724:7fafadbf16c7
    57           (decls, []) |-> fold (fn (name, decl) =>
    57           (decls, []) |-> fold (fn (name, decl) =>
    58             if exists (fn space => Name_Space.declared space name) parent_spaces then I
    58             if exists (fn space => Name_Space.declared space name) parent_spaces then I
    59             else
    59             else
    60               (case export name decl of
    60               (case export name decl of
    61                 NONE => I
    61                 NONE => I
    62               | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
    62               | SOME body =>
    63           |> sort_by #1 |> map #2
    63                   cons (#serial (Name_Space.the_entry space name),
       
    64                     XML.Elem (entity_markup space name, body))))
       
    65           |> sort (int_ord o apply2 #1) |> map #2
    64         end;
    66         end;
       
    67 
    65       in if null elems then () else export_body thy export_name elems end;
    68       in if null elems then () else export_body thy export_name elems end;
    66 
    69 
    67 
    70 
    68     (* types *)
    71     (* types *)
    69 
    72