diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/BNF_Fixpoint_Base.thy
--- a/src/HOL/BNF_Fixpoint_Base.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -131,10 +131,10 @@
 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
   by auto
 
-lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
+lemma eq_subset: "(=) \<le> (\<lambda>a b. P a b \<or> a = b)"
   by auto
 
-lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
+lemma eq_le_Grp_id_iff: "((=) \<le> Grp (Collect R) id) = (All R)"
   unfolding Grp_def id_apply by blast
 
 lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
@@ -211,10 +211,10 @@
   by simp
 
 lemma comp_transfer:
-  "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
+  "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (\<circ>) (\<circ>)"
   unfolding rel_fun_def by simp
 
-lemma If_transfer: "rel_fun (op =) (rel_fun A (rel_fun A A)) If If"
+lemma If_transfer: "rel_fun (=) (rel_fun A (rel_fun A A)) If If"
   unfolding rel_fun_def by simp
 
 lemma Abs_transfer: