--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Sep 12 20:31:28 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Sep 12 23:17:55 2016 +0200
@@ -104,7 +104,7 @@
[[[]], [@{thms setr.intros[OF refl]}]]],
set_cases = @{thms setl.cases[simplified hypsubst_in_prems]
setr.cases[simplified hypsubst_in_prems]}},
- fp_co_induct_sugar =
+ fp_co_induct_sugar = SOME
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
common_co_inducts = @{thms sum.induct},
co_inducts = @{thms sum.induct},
@@ -176,7 +176,7 @@
[[[], @{thms snds.intros[of "(a, b)" for a b, simplified snd_conv]}]]],
set_cases = @{thms fsts.cases[simplified eq_fst_iff ex_neg_all_pos]
snds.cases[simplified eq_snd_iff ex_neg_all_pos]}},
- fp_co_induct_sugar =
+ fp_co_induct_sugar = SOME
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},
co_inducts = @{thms prod.induct},