diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Aug 04 13:24:54 2024 +0200
@@ -204,7 +204,7 @@
     val atomTs = distinct op = (maps (map snd o #2) prems);
     val ind_sort = if null atomTs then \<^sort>\<open>type\<close>
       else Sign.minimize_sort thy (Sign.certify_sort thy (map (fn T => Sign.intern_class thy
-        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs));
+        ("fs_" ^ Long_Name.base_name (dest_Type_name T))) atomTs));
     val (fs_ctxt_tyname, _) = Name.variant "'n" (Variable.names_of ctxt');
     val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
@@ -276,7 +276,7 @@
 
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
-      ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
+      ("pt_" ^ Long_Name.base_name (dest_Type_name aT) ^ "2")) atomTs;
     fun eqvt_ss ctxt =
       put_simpset HOL_basic_ss ctxt
         addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
@@ -285,7 +285,7 @@
     val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
     val perm_bij = Global_Theory.get_thms thy "perm_bij";
     val fs_atoms = map (fn aT => Global_Theory.get_thm thy
-      ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
+      ("fs_" ^ Long_Name.base_name (dest_Type_name aT) ^ "1")) atomTs;
     val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
     val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
     val swap_simps = Global_Theory.get_thms thy "swap_simps";