src/HOL/Tools/BNF/bnf_lfp.ML
changeset 67399 eab6ce8368fa
parent 67091 1393c2340eec
child 67405 e9ab4ad7bd15
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -537,8 +537,8 @@
     1.4        ||>> mk_Frees "s" sTs
     1.5        ||>> mk_Frees "i" (replicate n suc_bdT)
     1.6        ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi"))
     1.7 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
     1.8 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT;
     1.9 +      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") suc_bdT
    1.10 +      ||>> yield_singleton (apfst (~~) oo mk_Frees' "j") suc_bdT;
    1.11  
    1.12      val suc_bd_limit_thm =
    1.13        let
    1.14 @@ -764,7 +764,7 @@
    1.15        lthy
    1.16        |> mk_Frees "IIB" II_BTs
    1.17        ||>> mk_Frees "IIs" II_sTs
    1.18 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
    1.19 +      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
    1.20        ||>> mk_Frees "x" init_FTs;
    1.21  
    1.22      val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
    1.23 @@ -816,7 +816,7 @@
    1.24        |> mk_Frees "B" BTs
    1.25        ||>> mk_Frees "s" sTs
    1.26        ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs)
    1.27 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
    1.28 +      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
    1.29        ||>> mk_Frees "ix" active_initTs
    1.30        ||>> mk_Frees' "x" init_FTs
    1.31        ||>> mk_Frees "f" init_fTs
    1.32 @@ -941,7 +941,7 @@
    1.33      val ((ss, (fold_f, fold_f')), _) =
    1.34        lthy
    1.35        |> mk_Frees "s" sTs
    1.36 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT;
    1.37 +      ||>> yield_singleton (apfst (~~) oo mk_Frees' "f") foldT;
    1.38  
    1.39      fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
    1.40      val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
    1.41 @@ -1279,7 +1279,7 @@
    1.42            (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors);
    1.43          val ctor_fold_ctors = (ctor_fold_unique_thm OF
    1.44            map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS
    1.45 -            @{thm trans[OF arg_cong2[of _ _ _ _ "op \<circ>", OF refl] o_id]}))) map_id0s)
    1.46 +            @{thm trans[OF arg_cong2[of _ _ _ _ "(\<circ>)", OF refl] o_id]}))) map_id0s)
    1.47            |> split_conj_thm |> map mk_sym;
    1.48        in
    1.49          infer_instantiate lthy theta ctor_fold_unique_thm