src/HOL/Tools/inductive_package.ML

         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
           rec_sets_defs thy1;
     val induct =
       if coind then
         (raw_induct, [RuleCases.case_names [rec_name],
-          RuleCases.case_conclusion_binops rec_name induct_cases,
+          RuleCases.case_conclusion (rec_name, induct_cases),
           RuleCases.consumes 1])
       else if no_ind orelse length cs > 1 then
         (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
       else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);