# HG changeset patch
# User wenzelm
# Date 1634411664 -7200
# Node ID 638301b86f0a26f8658052e0fd9467de8428cf11
# Parent  5cab031e2344899a67c5e9051584b5147ee79a7f
tuned;

diff -r 5cab031e2344 -r 638301b86f0a src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sat Oct 16 20:32:25 2021 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sat Oct 16 21:14:24 2021 +0200
@@ -622,8 +622,8 @@
         local open Conv in
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
-            fconv_rule (Conv.binder_conv
-              (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
+            fconv_rule
+              (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt1) aihyp
         end
 
         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih