--- 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;