src/HOL/Tools/BNF/bnf_lfp.ML
changeset 67091 1393c2340eec
parent 64413 c0d5e78eb647
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 26 22:40:28 2016 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -1279,7 +1279,7 @@
     1.4            (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors);
     1.5          val ctor_fold_ctors = (ctor_fold_unique_thm OF
     1.6            map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS
     1.7 -            @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]}))) map_id0s)
     1.8 +            @{thm trans[OF arg_cong2[of _ _ _ _ "op \<circ>", OF refl] o_id]}))) map_id0s)
     1.9            |> split_conj_thm |> map mk_sym;
    1.10        in
    1.11          infer_instantiate lthy theta ctor_fold_unique_thm