diff -r 75786c2eb897 -r bc5c6c9b114e src/FOLP/IFOLP.ML
--- a/src/FOLP/IFOLP.ML	Wed Feb 15 19:11:10 2006 +0100
+++ b/src/FOLP/IFOLP.ML	Wed Feb 15 21:34:55 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 gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
+          then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
                    [_] => assume_tac i
                  |  _  => no_tac
           else no_tac