# HG changeset patch
# User wenzelm
# Date 1132768321 -3600
# Node ID 0183318232f2b7538ddd6f08f3d157394bc672a5
# Parent  5a124c76e92fd10dcfccf0ca5e83cd03cb839e5d
RuleCases.case_conclusion;

diff -r 5a124c76e92f -r 0183318232f2 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Nov 23 18:52:00 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 23 18:52:01 2005 +0100
@@ -788,7 +788,7 @@
     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])