src/FOLP/IFOLP.thy

     (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 distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
+          then case distinct (=) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
                    [_] => assume_tac ctxt i
                  |  _  => no_tac
           else no_tac
       end);
 end;

   done
 
 lemmas pred_congs = pred1_cong pred2_cong pred3_cong
 
 (*special case for the equality predicate!*)
-lemmas eq_cong = pred2_cong [where P = "op ="]
+lemmas eq_cong = pred2_cong [where P = "(=)"]
 
 
 (*** Simplifications of assumed implications.
      Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
      used with mp_tac (restricted to atomic formulae) is COMPLETE for