diff -r 826a1ae59cac -r c6c2e41cac1c src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Dec 31 15:16:05 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Dec 31 16:15:27 2023 +0100
@@ -392,7 +392,7 @@
     val typ_map = Type.strip_sorts o
       Term_Subst.map_atypsT (fn U =>
         if member (op =) atyps U
-        then #unconstrain_typ ucontext {strip_sorts = false} U
+        then #typ_operation ucontext {strip_sorts = false} U
         else raise Same.SAME);
     fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
     val xs' = map (map_types typ_map) xs