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