--- a/src/HOL/Tools/record.ML Wed Sep 17 21:35:58 2014 +0200
+++ b/src/HOL/Tools/record.ML Wed Sep 17 23:45:28 2014 +0200
@@ -1781,15 +1781,15 @@
end
else thy;
-fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms =
+fun add_ctr_sugar ctr exhaust inject sel_thms =
Ctr_Sugar.default_register_ctr_sugar_global (K true)
- {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels],
+ {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_defs, sel_thmss = [sel_thms], distinct_discsss = [],
- exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [],
- split_sel_asms = [], case_eq_ifs = []};
+ discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [],
+ exhaust_sels = [], collapses = [], expands = [], split_sels = [], split_sel_asms = [],
+ case_eq_ifs = []};
(* definition *)
@@ -2235,7 +2235,7 @@
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) names
|> add_code ext_tyco vs extT ext simps' ext_inject
- |> add_ctr_sugar (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
+ |> add_ctr_sugar (Const ext) cases_scheme' ext_inject sel_convs'
|> Sign.restore_naming thy;
in final_thy end;