- let qs = proc_bkd_proofs (next st) synth names classes tl in
- if is_rewrite_right hd then
- script @ mk_rewrite st dtext where qs tl false what
+ let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
+ if List.length qs <> List.length names then
+ let qs = proc_bkd_proofs (next st) synth [] classes tl in
+ let hd = mk_exp_args hd tl classes synth in
+ script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+ else if is_rewrite_right hd then
+ script2 @ mk_rewrite st dtext where qs tl2 false what