src/HOL/Tools/record.ML

      case_distribs = [], split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [],
      disc_thmss = [], discIs = [], disc_eq_cases = [], sel_defs = [], sel_thmss = [sel_thms],
      distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
      split_sels = [], split_sel_asms = [], case_eq_ifs = []};
 
+fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t
+  | lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t;
+
+fun add_spec_rule rule =
+  let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in
+    Spec_Rules.add_global Spec_Rules.Equational ([head], [rule])
+  end;
 
 (* definition *)
 
 fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
   let

                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) sel_specs
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
           ||>> (Global_Theory.add_defs false o
                 map (rpair [Code.add_default_eqn_attribute]
-                o apfst (Binding.concealed o Binding.name))) (*FIXME Spec_Rules (?)*)
+                o apfst (Binding.concealed o Binding.name)))
             [make_spec, fields_spec, extend_spec, truncate_spec]);
     val defs_ctxt = Proof_Context.init_global defs_thy;
 
     (* prepare propositions *)
     val _ = timing_msg defs_ctxt "record preparing propositions";

     val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
     val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
 
     (*selectors*)
     val sel_conv_props =
-       map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
+      map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
 
     (*updates*)
     fun mk_upd_prop i (c, T) =
       let
         val x' =

       make_info alphas parent fields extension
         ext_induct ext_inject ext_surjective ext_split ext_def
         sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
         surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
 
-    val sels = map (fst o Logic.dest_equals o Thm.prop_of) sel_defs;
-
     val final_thy =
       thms_thy'
       |> put_record name info
       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs
       |> add_equalities extension_id equality'

       |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
       |> 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) cases_scheme' ext_inject sel_convs'
+      |> fold add_spec_rule (sel_convs' @ upd_convs' @ derived_defs')
       |> Sign.restore_naming thy0;
 
   in final_thy end;