make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
in
[B.H([],
- (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+ (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*)
+ (B.b_kw "by")::
B.b_space::
B.Text([],"(")::pres_args@[B.Text([],")")])], None
else