diff -r d9cf62ea273d -r e1895596e1b9 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Dec 31 18:49:00 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Dec 31 19:24:37 2023 +0100
@@ -390,7 +390,7 @@
     val cs = maps (fn T => map (pair T) S) Ts;
     val constraints' = map Logic.mk_of_class cs;
     val typ_map = Type.strip_sorts o
-      Term_Subst.map_atypsT (fn U =>
+      Term.map_atyps (fn U =>
         if member (op =) atyps U
         then #typ_operation ucontext {strip_sorts = false} U
         else raise Same.SAME);