changeset 33039 | 5018f6a76b3f |
parent 33035 | 15eab423e573 |
parent 33038 | 8f9594c31de4 |
child 33042 | ddf1f03a9ad9 |
--- a/src/HOL/Tools/metis_tools.ML Wed Oct 21 16:41:22 2009 +1100 +++ b/src/HOL/Tools/metis_tools.ML Wed Oct 21 08:16:25 2009 +0200 @@ -631,7 +631,7 @@ let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith in {axioms = (mth, Meson.make_meta_clause ith) :: axioms, - tfrees = tfree_lits union tfrees} + tfrees = union (op =) (tfree_lits, tfrees)} end; val lmap0 = List.foldl (add_thm true) {axioms = [], tfrees = init_tfrees ctxt} cls