changeset 9898 | 5f28e5b4c68e |
parent 9705 | 8eecca293907 |
child 10008 | 61eb9f3aa92a |
--- a/src/HOL/Tools/record_package.ML Thu Sep 07 20:53:50 2000 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Sep 07 20:55:18 2000 +0200 @@ -829,7 +829,7 @@ ("select_convs", sel_convs), ("update_convs", update_convs)] |> (#1 oo (PureThy.add_thms o map Thm.no_attributes)) - [("equality", equality)] + [("equality", equality)] |> (#1 oo PureThy.add_thmss) [(("simps", simps), [Simplifier.simp_add_global]), (("iffs", iffs), [iff_add_global])];