src/HOL/Tools/BNF/bnf_lfp.ML

       lthy
       |> mk_Frees "B" BTs
       ||>> mk_Frees "s" sTs
       ||>> mk_Frees "i" (replicate n suc_bdT)
       ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi"))
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT;
+      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") suc_bdT
+      ||>> yield_singleton (apfst (~~) oo mk_Frees' "j") suc_bdT;
 
     val suc_bd_limit_thm =
       let
         val prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map (fn idx => HOLogic.mk_mem (idx, field_suc_bd)) idxs));

 
     val ((((II_Bs, II_ss), (iidx, iidx')), init_xFs), _) =
       lthy
       |> mk_Frees "IIB" II_BTs
       ||>> mk_Frees "IIs" II_sTs
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
+      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
       ||>> mk_Frees "x" init_FTs;
 
     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
       (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
         Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),

         init_fs_copy), init_phis), _) =
       lthy
       |> mk_Frees "B" BTs
       ||>> mk_Frees "s" sTs
       ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs)
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
+      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
       ||>> mk_Frees "ix" active_initTs
       ||>> mk_Frees' "x" init_FTs
       ||>> mk_Frees "f" init_fTs
       ||>> mk_Frees "f" init_fTs
       ||>> mk_Frees "P" (replicate n (mk_pred1T initT));

     val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
 
     val ((ss, (fold_f, fold_f')), _) =
       lthy
       |> mk_Frees "s" sTs
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT;
+      ||>> yield_singleton (apfst (~~) oo mk_Frees' "f") foldT;
 
     fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
     val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
 
     fun ctor_spec abs str map_FT_init =

         fun mk_fun_insts T ix = Thm.cterm_of lthy (Var (ix, T --> T));
         val theta =
           (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors);
         val ctor_fold_ctors = (ctor_fold_unique_thm OF
           map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS
-            @{thm trans[OF arg_cong2[of _ _ _ _ "op \<circ>", OF refl] o_id]}))) map_id0s)
+            @{thm trans[OF arg_cong2[of _ _ _ _ "(\<circ>)", OF refl] o_id]}))) map_id0s)
           |> split_conj_thm |> map mk_sym;
       in
         infer_instantiate lthy theta ctor_fold_unique_thm
         |> unfold_thms lthy ctor_fold_ctors
         |> Morphism.thm (Local_Theory.target_morphism lthy)