diff -r d589d1d218b2 -r ec50b9213969 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Apr 14 22:08:16 2023 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Apr 14 22:19:28 2023 +0200
@@ -279,7 +279,7 @@
 val add_typeof_eqns = gen_add_typeof_eqns read_condeq;
 
 fun thaw (T as TFree (a, S)) =
-      if exists_string (fn s => s = ":") a then TVar (unpack_ixn a, S) else T
+      if member_string a ":" then TVar (unpack_ixn a, S) else T
   | thaw (Type (a, Ts)) = Type (a, map thaw Ts)
   | thaw T = T;