--- a/src/Pure/Proof/extraction.ML Wed Dec 27 21:42:42 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Dec 29 15:58:43 2023 +0100
@@ -390,7 +390,7 @@
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);
+ (map_atyps (fn U => if member (op =) atyps U then #atyp_map ucontext U else U) T);
fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
val xs' = map (map_types typ_map) xs
in