src/HOL/Tools/datatype_realizer.ML

     val ind_name = Thm.derivation_name induct;
     val vs = map (nth pnames) is;
     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])) []);
     val rvs = rev (Thm.fold_terms {hyps = false} Term.add_vars thm' []);
     val ivs1 = map Var (filter_out (fn (_, T) => \<^type_name>\<open>bool\<close> = tname_of (body_type T)) ivs);

       |> Drule.export_without_context;
 
     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);
     val prf =
       Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]