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