diff -r 7849b6370425 -r 505f97165f52 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Fri Jul 19 11:29:05 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Fri Jul 19 16:58:52 2024 +0200
@@ -283,8 +283,8 @@
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
-      if #serial header = #serial thm_id then Thm_Name.empty
-      else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
+      if #serial header = #serial thm_id then Thm_Name.none
+      else the_default Thm_Name.none (lookup_thm_id (Proofterm.thm_header_id header));
 
     fun entity_markup_thm (serial, (name, i)) =
       let
@@ -314,7 +314,7 @@
           in triple encode_prop (list Thm_Name.encode) encode_proof end
       end;
 
-    fun export_thm (thm_id, thm_name) =
+    fun export_thm (thm_id, (thm_name, _)) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val body =