src/HOL/Option.thy

   "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
     Option.bind Option.bind"
   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