--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:04 2014 +0200
@@ -90,7 +90,8 @@
rel_intros = [],
rel_cases = [],
set_thms = [],
- set_sels = []},
+ set_sels = [],
+ set_intros = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
common_co_inducts = @{thms sum.induct},
@@ -141,7 +142,8 @@
rel_intros = [],
rel_cases = [],
set_thms = [],
- set_sels = []},
+ set_sels = [],
+ set_intros = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},