diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Tue Oct 19 14:41:29 2021 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Tue Oct 19 14:58:22 2021 +0200
@@ -384,7 +384,8 @@
 fun transfer_rel_conv conv =
   Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)));
 
-fun fold_relator_eqs_conv ctxt ct = (Transfer.bottom_rewr_conv (Transfer.get_relator_eq ctxt)) ct;
+fun fold_relator_eqs_conv ctxt =
+  Conv.bottom_rewrs_conv (Transfer.get_relator_eq ctxt) ctxt;
 
 fun mk_is_equality t =
   Const (\<^const_name>\<open>is_equality\<close>, Term.fastype_of t --> HOLogic.boolT) $ t;