src/HOL/Tools/BNF/bnf_comp.ML
changeset 67091 1393c2340eec
parent 65436 1fd2dca8eb60
child 68960 b85d509e7cbf
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -932,7 +932,7 @@
     1.4         rtac ctxt refl) 1;
     1.5      fun pred_set_tac ctxt =
     1.6        HEADGOAL (EVERY'
     1.7 -        [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f o _"]} RS trans),
     1.8 +        [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\<lambda>f. f \<circ> _"]} RS trans),
     1.9          SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]);
    1.10  
    1.11      val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac