--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:36 2014 +0200
@@ -88,7 +88,8 @@
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
rel_sels = [],
rel_intros = [],
- rel_cases = []},
+ rel_cases = [],
+ set_thms = []},
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},
@@ -137,7 +138,8 @@
rel_distincts = [],
rel_sels = [],
rel_intros = [],
- rel_cases = []},
+ rel_cases = [],
+ set_thms = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},