--- a/src/HOL/Tools/record.ML Mon Jan 05 00:07:01 2015 +0100
+++ b/src/HOL/Tools/record.ML Fri Dec 19 11:17:23 2014 +0100
@@ -1786,10 +1786,10 @@
{kind = Ctr_Sugar.Record, T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy,
discs = [], selss = [], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject],
distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
- split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [],
- discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [],
- exhaust_sels = [], collapses = [], expands = [], split_sels = [], split_sel_asms = [],
- case_eq_ifs = []};
+ case_distribs = [], split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [],
+ disc_thmss = [], discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [],
+ exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [],
+ split_sel_asms = [], case_eq_ifs = []};
(* definition *)