src/Pure/Thy/export_theory.ML

           val body = encode_locale_dependency dep;
         in XML.Elem (markup, body) end)
       |> 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 _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
         [YXML.string_of_body (XML.Encode.string (cat_lines (map Context.theory_long_name parents)))];