changeset 18977 | f24c416a4814 |
parent 17480 | fd19f77dcf60 |
child 19046 | bc5c6c9b114e |
--- a/src/FOLP/IFOLP.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/FOLP/IFOLP.ML Wed Feb 08 14:39:00 2006 +0100 @@ -77,7 +77,7 @@ and concl = discard_proof (Logic.strip_assums_concl prem) in if exists (fn hyp => hyp aconv concl) hyps - then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of + then case gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of [_] => assume_tac i | _ => no_tac else no_tac