changeset 33042 | ddf1f03a9ad9 |
parent 33038 | 8f9594c31de4 |
child 33043 | ff71cadefb14 |
--- a/src/HOL/Import/shuffler.ML Wed Oct 21 12:02:19 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Wed Oct 21 12:02:56 2009 +0200 @@ -78,7 +78,7 @@ val empty = [] val copy = I val extend = I - fun merge _ = Library.union Thm.eq_thm + fun merge _ = Library.merge Thm.eq_thm_prop ) fun print_shuffles thy =