src/FOLP/IFOLP.ML

     (fn (prem,i) =>
       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
           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
       end);
 end;