diff -r 276b07a1b5f5 -r a90ab1ea6458 src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/functor.ML	Sun Aug 04 13:24:54 2024 +0200
@@ -209,10 +209,10 @@
     val (Ts, T1, T2) = split_mapper_typ tyco T
       handle List.Empty => bad_typ ();
     val _ =
-      apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
+      apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o dest_Type_name) (T1, T2)
         handle TYPE _ => bad_typ ();
     val (vs1, vs2) =
-      apply2 (map dest_TFree o snd o dest_Type) (T1, T2)
+      apply2 (map dest_TFree o dest_Type_args) (T1, T2)
         handle TYPE _ => bad_typ ();
     val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
       then bad_typ () else ();