src/HOL/Tools/choice_specification.ML

--- a/src/HOL/Tools/choice_specification.ML	Tue Dec 05 20:07:52 2023 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Tue Dec 05 20:56:51 2023 +0100
@@ -57,10 +57,10 @@
 fun unvarify_global t fmap =
   let
     val fmap' = map Library.swap fmap
-    fun unthaw (f as (a, S)) =
-      (case AList.lookup (op =) fmap' a of
-        NONE => TVar f
-      | SOME (b, _) => TFree (b, S))
+    fun unthaw v =
+      (case AList.lookup (op =) fmap' v of
+        NONE => TVar v
+      | SOME w => TFree w)
   in map_types (map_type_tvar unthaw) t end