src/HOL/Tools/BNF/bnf_fp_util_tactics.ML

--- a/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML	Wed Jan 10 15:25:09 2018 +0100
@@ -30,7 +30,7 @@
   ALLGOALS (rtac ctxt refl);
 
 fun mk_conj_arg_congN 1 = @{thm DEADID.rel_mono_strong}
-  | mk_conj_arg_congN n = mk_conj_arg_congN (n - 1) RSN (2, @{thm arg_cong2[of _ _ _ _ "op \<and>"]});
+  | mk_conj_arg_congN n = mk_conj_arg_congN (n - 1) RSN (2, @{thm arg_cong2[of _ _ _ _ "(\<and>)"]});
 
 fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps =
   HEADGOAL (rtac ctxt (mk_conj_arg_congN (length xtor_un_fold_xtors) RS iffD1 OF
@@ -87,4 +87,4 @@
           etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer})))
       (defs ~~ un_fold_transfers));
 
-end
\ No newline at end of file
+end