diff -r cf32eb8001b8 -r a5c08cd60a3f src/HOL/Tools/record.ML
--- 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;