src/FOLP/IFOLP.ML
changeset 18977 f24c416a4814
parent 17480 fd19f77dcf60
child 19046 bc5c6c9b114e
equal deleted inserted replaced
18976:4efb82669880 18977:f24c416a4814
    75     (fn (prem,i) =>
    75     (fn (prem,i) =>
    76       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
    76       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
    77           and concl = discard_proof (Logic.strip_assums_concl prem)
    77           and concl = discard_proof (Logic.strip_assums_concl prem)
    78       in
    78       in
    79           if exists (fn hyp => hyp aconv concl) hyps
    79           if exists (fn hyp => hyp aconv concl) hyps
    80           then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
    80           then case gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
    81                    [_] => assume_tac i
    81                    [_] => assume_tac i
    82                  |  _  => no_tac
    82                  |  _  => no_tac
    83           else no_tac
    83           else no_tac
    84       end);
    84       end);
    85 end;
    85 end;