src/HOL/Nominal/nominal_inductive.ML

--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 07 14:44:51 2024 +0200
@@ -250,7 +250,7 @@
       end) prems);
 
     val ind_vars =
-      (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+      (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
        map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
     val ind_Ts = rev (map snd ind_vars);