--- a/src/Pure/Proof/extraction.ML Sat Dec 30 15:59:11 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Dec 30 17:19:31 2023 +0100
@@ -389,8 +389,11 @@
(build_rev (Term.add_vars prop'));
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
- fun typ_map T = Type.strip_sorts
- (map_atyps (fn U => if member (op =) atyps U then #atyp_map ucontext U else U) T);
+ val typ_map = Type.strip_sorts o
+ Same.commit (Term_Subst.map_atypsT_same (fn U =>
+ if member (op =) atyps U
+ then #unconstrain_typ 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
in