--- a/src/FOLP/IFOLP.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/FOLP/IFOLP.thy Wed Jan 10 15:25:09 2018 +0100
@@ -259,7 +259,7 @@
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
@@ -522,7 +522,7 @@
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.