--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:36:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:36:48 2014 +0200
@@ -109,7 +109,8 @@
co_rec_transfers = [],
common_rel_co_inducts = [],
rel_co_inducts = [],
- common_set_inducts = []}}
+ common_set_inducts = [],
+ set_inducts = []}}
end;
fun fp_sugar_of_prod ctxt =
@@ -171,7 +172,8 @@
co_rec_transfers = [],
common_rel_co_inducts = [],
rel_co_inducts = [],
- common_set_inducts = []}}
+ common_set_inducts = [],
+ set_inducts = []}}
end;
val _ = Theory.setup (map_local_theory (fn lthy =>