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