author | wenzelm |
Tue, 15 Feb 2000 19:41:44 +0100 | |
changeset 8246 | efb3c8253d90 |
parent 8245 | 6acc80f7f36f |
child 8247 | 635339ef2dca |
--- 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;