--- 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);