src/HOL/Tools/Function/function_core.ML

 
         val case_hyp_conv = K (case_hyp RS eq_reflection)
         local open Conv in
           val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
           val sih =
-            fconv_rule (More_Conv.binder_conv
+            fconv_rule (Conv.binder_conv
               (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
         end
 
         fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
           |> forall_elim (cterm_of thy rcarg)