src/HOL/Tools/BNF/bnf_lift.ML
changeset 67091 1393c2340eec
parent 66272 c6714a9562ae
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -310,7 +310,7 @@
     1.4  
     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})),
    1.10                  rtac ctxt refl]);
    1.11