--- a/src/Pure/Thy/export_theory.ML Sun Oct 20 22:26:44 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML Mon Oct 21 16:32:10 2019 +0200
@@ -399,6 +399,20 @@
|> export_body thy "locale_dependencies";
+ (* constdefs *)
+
+ val constdefs =
+ Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy)
+ |> sort_by #1;
+
+ val encode_constdefs =
+ let open XML.Encode
+ in list (pair string string) end;
+
+ val _ =
+ if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
+
+
(* parents *)
val _ =