diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/Build/export_theory.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -263,7 +263,7 @@
         val args' = args |> filter (is_free o #1);
         val typargs' = typargs |> filter (is_free o #1);
         val used_typargs = fold (Name.declare o #1) typargs' used;
-        val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
+        val sorts = Name.invent_types used_typargs extra_shyps;
       in ((sorts @ typargs', args', prop), proof) end;
 
     fun standard_prop_of thm =