src/HOL/Tools/record_package.ML
changeset 8246 efb3c8253d90
parent 8168 9d2ac5439089
child 8274 0d8fa545bd5c
--- 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;