--- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 26 21:08:32 2017 +0100
@@ -932,7 +932,7 @@
rtac ctxt refl) 1;
fun pred_set_tac ctxt =
HEADGOAL (EVERY'
- [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f o _"]} RS trans),
+ [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans),
SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]);
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac