--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jan 11 13:48:17 2018 +0100
@@ -537,8 +537,8 @@
||>> 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 (~~) oo mk_Frees' "i") suc_bdT
- ||>> yield_singleton (apfst (~~) oo mk_Frees' "j") suc_bdT;
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT;
val suc_bd_limit_thm =
let
@@ -764,7 +764,7 @@
lthy
|> mk_Frees "IIB" II_BTs
||>> mk_Frees "IIs" II_sTs
- ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
+ ||>> yield_singleton (apfst (op ~~) 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)
@@ -816,7 +816,7 @@
|> mk_Frees "B" BTs
||>> mk_Frees "s" sTs
||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs)
- ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
||>> mk_Frees "ix" active_initTs
||>> mk_Frees' "x" init_FTs
||>> mk_Frees "f" init_fTs
@@ -941,7 +941,7 @@
val ((ss, (fold_f, fold_f')), _) =
lthy
|> mk_Frees "s" sTs
- ||>> yield_singleton (apfst (~~) oo mk_Frees' "f") foldT;
+ ||>> yield_singleton (apfst (op ~~) 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;