changeset 33042 | ddf1f03a9ad9 |
parent 33038 | 8f9594c31de4 |
child 33522 | 737589bb9bb8 |
--- a/src/HOL/Import/hol4rews.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Wed Oct 21 12:02:56 2009 +0200 @@ -165,7 +165,7 @@ val empty = [] val copy = I val extend = I - fun merge _ = Library.union Thm.eq_thm + fun merge _ = Library.merge Thm.eq_thm_prop ) val hol4_debug = Unsynchronized.ref false