diff --git a/src/Invariants.ml b/src/Invariants.ml
index 34302d9..12d8c7d 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -273,7 +273,6 @@ let split do_postcond avs ans negchi_locs bvs cand_bvs q =
   let negbs =
     if do_postcond then q.negbs
     else List.filter (fun b->not (q.is_chiK (q.find_chi b))) q.negbs in
-  let renaming = ref [] in
   let rec loop avs ans discard sol =
     (* 2 *)
     (*[* Format.printf "split-loop: starting@ avs=%a@\nans=@ %a@\nsol=@ %a@\n%!"
@@ -400,7 +399,6 @@ let split do_postcond avs ans negchi_locs bvs cand_bvs q =
       avss in
     (* 13 *)
     let ans_p = List.concat ans_rs in
-    renaming := update_sb ~more_sb:ans_p !renaming;
     (*[* Format.printf "split: ans_p=@ %a@ --@ ans_res=@ %a@\n%!"
       pr_subst ans_p pr_formula ans_res; *]*)
     let ans_res = to_formula ans_p @ subst_formula ans_p ans_res in
@@ -428,7 +426,7 @@ let split do_postcond avs ans negchi_locs bvs cand_bvs q =
   let solT = List.map (fun b->b, []) negbs in
   let ans_res, discard, sol =
     loop (vars_of_list avs) ans [] solT in
-  !renaming, ans_res, discard, sol
+  ans_res, discard, sol
 
 (** Eliminate provided variables if they do not contribute to
     constraints and generally simplify the formula. *)
@@ -787,7 +785,7 @@ let solve q_ops new_ex_types exty_res_chi brs =
       (fun i -> i, ([], []))
       (Ints.elements q.allchi) in
   let rolT, solT = List.partition (q.is_chiK % fst) solT in
-  let rec loop iter_no discard renaming1 rol1 sol1 =
+  let rec loop iter_no discard rol1 sol1 =
     (* 1 *)
     let sol1 = List.map
         (fun (i,(vs,ans)) -> i,(vs,remove_alphaK ans)) sol1 in
@@ -824,8 +822,8 @@ let solve q_ops new_ex_types exty_res_chi brs =
            else Some
                (nonrec, chiK, vK, prem, allconcl))
         brs1 in
-    (*[* Format.printf "solve: loop iter_no=%d@\nrenaming=%a@\nsol=@ %a@\n%!"
-      iter_no pr_subst renaming1 pr_chi_subst sol1; *]*)
+    (*[* Format.printf "solve: loop iter_no=%d@\nsol=@ %a@\n%!"
+      iter_no pr_chi_subst sol1; *]*)
     (*[* Format.printf "brs=@ %a@\n%!" Infer.pr_rbrs5 brs1; *]*)
     let validate ans = List.iter
         (fun (nonrec, _, _, prem, concl) ->
@@ -1095,13 +1093,13 @@ let solve q_ops new_ex_types exty_res_chi brs =
                    pr_exception e; *]*)
                  ())
             neg_cns1;
-        let renaming, ans_res, more_discard, ans_sol =
+        let ans_res, more_discard, ans_sol =
           split (iter_no>0 || !early_postcond_abd)
             vs ans negchi_locs bvs cand_bvs q in
         (*[* Format.printf
           "solve: loop -- answer split@ more_discard=@ %a@\nans_res=@ %a@\n%!"
           pr_formula more_discard pr_formula ans_res; *]*)
-        Aux.Right (renaming, alien_eqs, ans_res, more_discard, ans_sol)
+        Aux.Right (alien_eqs, ans_res, more_discard, ans_sol)
       with
       (* it does not seem to make a difference *)
       | (NoAnswer (sort, msg, tys, lc)
@@ -1113,15 +1111,14 @@ let solve q_ops new_ex_types exty_res_chi brs =
         Aux.Left (sort, e) in
     match answer with
     | Aux.Left _ as e -> e
-    | Aux.Right (renaming, alien_eqs, ans_res, more_discard, ans_sol) ->
+    | Aux.Right (alien_eqs, ans_res, more_discard, ans_sol) ->
       let more_discard =
         if alien_eqs = [] then more_discard
-        (* FIXME: not substituting [renaming]? *)
         else subst_formula alien_eqs more_discard in
       (* 12 *)
-      let finish renaming2 rol2 sol2 =
+      let finish rol2 sol2 =
         (* start fresh at (iter_no+1) *)
-        match loop (iter_no+1) empty_dl renaming2 rol2 sol2
+        match loop (iter_no+1) empty_dl rol2 sol2
         with Aux.Right _ as res -> res
            | Aux.Left (sort, e) ->
              (*[* Format.printf
@@ -1164,7 +1161,7 @@ let solve q_ops new_ex_types exty_res_chi brs =
                  {discard with at_typ=s_discard.at_typ::discard.at_typ}
                | Num_sort ->
                  {discard with at_num=s_discard.at_num::discard.at_num} in
-             loop iter_no discard renaming1 rol1 sol1 in
+             loop iter_no discard rol1 sol1 in
       (* 9 *)
       (* Avoid substituting [bvs] -- treat them like leftmost. *)
       let cmp_v v1 v2 =
@@ -1296,24 +1293,12 @@ let solve q_ops new_ex_types exty_res_chi brs =
                      finished1 && finished2 && finished3 in
       (*[* Format.printf "solve-loop: finished 1=%b, 2=%b, 3=%b, r=%b@\n%!"
         finished1 finished2 finished3 finished; *]*)
-      let param_sb = map_some
-        (fun (v, sv) ->
-          try match List.assoc v alien_eqs with
-            | TVar v3, _ -> Some (v3, sv)
-            | _ -> None
-          with Not_found -> None)
-        renaming in
-      let alien_eqs2 = subst_sb param_sb alien_eqs in
-      let renaming2 =
-        update_sb ~more_sb:renaming
-          (update_sb ~more_sb:alien_eqs2
-             (update_sb param_sb renaming1)) in
       if iter_no > 1 && finished
       then                              (* final solution *)
         Aux.Right (ans_res, rol2, sol2)
         (* Do at least three iterations: 0, 1, 2. *)
       else if iter_no <= 1 && finished
-      then loop (iter_no+1) empty_dl renaming2 rol2 sol1
+      then loop (iter_no+1) empty_dl rol2 sol1
       else if iter_no >= !timeout_count
       then
         let unfinished1 =
@@ -1340,8 +1325,8 @@ let solve q_ops new_ex_types exty_res_chi brs =
                unfinished1 @ unfinished2 @ unfinished3) in
         timeout_flag := true;
         raise (NoAnswer (Type_sort, "Answers do not converge", None, loc))
-      else finish renaming2 rol2 sol2 in
-  match loop 0 empty_dl [] rolT solT with
+      else finish rol2 sol2 in
+  match loop 0 empty_dl rolT solT with
   | Aux.Left (_, e) -> raise e
   | Aux.Right (ans_res, rol, sol) ->
     (*[* Format.printf "solve: checking assert false@\n%!"; *]*)