--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 13 09:21:15 2015 +0200
@@ -164,7 +164,7 @@
set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos]
snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}},
fp_co_induct_sugar =
- {co_rec = Const (@{const_name uncurry}, (ctr_Ts ---> C) --> fpT --> C),
+ {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},
co_inducts = @{thms prod.induct},
co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},