tuned;
authorwenzelm
Sat, 16 Oct 2021 21:14:24 +0200
changeset 74921 638301b86f0a
parent 74920 5cab031e2344
child 74922 2f8e8dc9b522
tuned;
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