diff -r 692095bafcd9 -r 1e0ad25c94c8 src/Pure/Thy/export_theory.ML
--- 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 _ =