diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Aug 04 13:24:54 2024 +0200
@@ -227,7 +227,7 @@
       end) (Logic.strip_imp_prems raw_induct' ~~ induct_cases');
 
     val atomTs = distinct op = (maps (map snd o #2) prems);
-    val atoms = map (fst o dest_Type) atomTs;
+    val atoms = map dest_Type_name atomTs;
     val ind_sort = if null atomTs then \<^sort>\<open>type\<close>
       else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn a => Sign.intern_class thy
         ("fs_" ^ Long_Name.base_name a)) atoms));
@@ -321,7 +321,7 @@
         fun protect t =
           let val T = fastype_of t in Const (\<^const_name>\<open>Fun.id\<close>, T --> T) $ t end;
         val p = foldr1 HOLogic.mk_prod (map protect ts);
-        val atom = fst (dest_Type T);
+        val atom = dest_Type_name T;
         val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
         val fs_atom = Global_Theory.get_thm thy
           ("fs_" ^ Long_Name.base_name atom ^ "1");