diff -r 58073f3d748a -r 5335b1ca6233 src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Mon Dec 02 20:35:12 2024 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML	Mon Dec 02 22:16:29 2024 +0100
@@ -246,7 +246,7 @@
     val i = maxidx_of_term t + 1;
     fun tvar_to_tfree ((name, _), sort) = (name, sort);
     val tvars = Term.add_tvars t [];
-    val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars));
+    val new_frees = map TFree (Term.variant_bounds t (map tvar_to_tfree tvars));
     val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t;
     val T = fastype_of t;
     val U = fastype_of u;