--- a/src/HOL/Tools/record_package.ML Sat Oct 27 00:05:50 2001 +0200
+++ b/src/HOL/Tools/record_package.ML Sat Oct 27 00:06:22 2001 +0200
@@ -878,7 +878,7 @@
(("cases", cases), [RuleCases.case_names [fieldsN],
InductAttrib.cases_type_global name])];
- val simps = field_simps @ sel_convs' @ update_convs' @ [equality'];
+ val simps = sel_convs' @ update_convs' @ [equality'];
val iffs = field_injects;
val thms_thy' =
@@ -891,7 +891,8 @@
val final_thy =
thms_thy'
- |> put_record name (make_record_info args parent fields simps induct_scheme' cases_scheme')
+ |> put_record name (make_record_info args parent fields (field_simps @ simps)
+ induct_scheme' cases_scheme')
|> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs')
|> Theory.parent_path;