changeset 33043 | ff71cadefb14 |
parent 33040 | cffdb7b28498 |
parent 33042 | ddf1f03a9ad9 |
child 33245 | 65232054ffd0 |
--- a/src/HOL/Import/shuffler.ML Wed Oct 21 10:15:31 2009 +0200 +++ b/src/HOL/Import/shuffler.ML Wed Oct 21 12:08:52 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 =