diff -r eec06d39e5fa -r 8a9588ffc133 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -127,7 +127,8 @@
     val (thm', thy') = thy
       |> Sign.root_path
       |> Global_Theory.store_thm
-        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+        (Binding.qualified_name
+          (space_implode "_" (Thm_Name.short ind_name :: vs @ ["correctness"])), thm)
       ||> Sign.restore_naming thy;
 
     val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
@@ -201,7 +202,8 @@
     val exh_name = Thm.derivation_name exhaust;
     val (thm', thy') = thy
       |> Sign.root_path
-      |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
+      |> Global_Theory.store_thm
+          (Binding.qualified_name (Thm_Name.short exh_name ^ "_P_correctness"), thm)
       ||> Sign.restore_naming thy;
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);