--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:15 2014 +0200
@@ -86,7 +86,8 @@
map_sels = [],
rel_injects = @{thms rel_sum_simps(1,4)},
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
- rel_sels = []},
+ rel_sels = [],
+ rel_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},
@@ -133,7 +134,8 @@
map_sels = [],
rel_injects = @{thms rel_prod_apply},
rel_distincts = [],
- rel_sels = []},
+ rel_sels = [],
+ rel_intros = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},