# HG changeset patch
# User wenzelm
# Date 1004133982 -7200
# Node ID ed914e8a0fd11301710662d12499fbf3a2b7e374
# Parent  2ece34b9fd8e36d8caf7e7787e0e1af517cd5a16
exclude field_simps from user-level "simps";

diff -r 2ece34b9fd8e -r ed914e8a0fd1 src/HOL/Tools/record_package.ML
--- 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;