# HG changeset patch
# User wenzelm
# Date 1703861923 -3600
# Node ID e31b48b47e88baa094b9b129a512a3bcee948bc9
# Parent  664d378c18bc50f74cb8dd920446712a55bc99ae
tuned;

diff -r 664d378c18bc -r e31b48b47e88 src/Pure/Proof/extraction.ML
--- 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