# HG changeset patch
# User wenzelm
# Date 950640104 -3600
# Node ID efb3c8253d90cc02b88af9ad520bd0d3da26d487
# Parent  6acc80f7f36f8a664edef0c4a825592b5b769921
fixed sel_upd simproc (less efficient, but more complete);

diff -r 6acc80f7f36f -r efb3c8253d90 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Feb 15 17:51:11 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Feb 15 19:41:44 2000 +0100
@@ -827,7 +827,7 @@
     val final_thy =
       thms_thy
       |> put_record name {args = args, parent = parent, fields = fields, simps = simps}
-      |> put_sel_upd names (simps @ update_defs)
+      |> put_sel_upd names (field_simps @ sel_defs @ update_defs)
       |> add_record_splits named_splits
       |> Theory.parent_path;