src/HOL/Option.thy

--- a/src/HOL/Option.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Option.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -323,7 +323,7 @@
   unfolding rel_fun_def split_option_all by simp
 
 lemma pred_option_parametric [transfer_rule]:
-  "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
+  "((A ===> (=)) ===> rel_option A ===> (=)) pred_option pred_option"
   by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)
 
 end