src/HOL/Library/conditional_parametricity.ML

     val ctxt = fold (Variable.declare_typ o snd) (Term.add_frees t []) ctxt;
     val t = singleton (Variable.polymorphic ctxt) t;
     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;
     val R = [T,U] ---> \<^typ>\<open>bool\<close>
     val r = Var (("R", 2 * i), R);