exclude field_simps from user-level "simps";

--- 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;