diff --git a/src/coretypes/DefnBase.sml b/src/coretypes/DefnBase.sml
index 863029b32e..19c909f5ac 100644
--- a/src/coretypes/DefnBase.sml
+++ b/src/coretypes/DefnBase.sml
@@ -304,7 +304,8 @@ fun cases_prove case_const_def th k t =
             end
           else if is_exists (concl th) then
             let val (v, bod) = dest_exists (concl th)
-                val v' = variant (free_vars t) v
+                val avoids = op_union aconv (free_vars t) (free_vars (concl th))
+                val v' = variant avoids v
                 val bod' = subst[v |-> v'] bod
                 val t_th = recurse (ASSUME bod')
             in
diff --git a/src/num/theories/selftest.sml b/src/num/theories/selftest.sml
index 5967079fdd..b83700cf8c 100644
--- a/src/num/theories/selftest.sml
+++ b/src/num/theories/selftest.sml
@@ -89,6 +89,20 @@ val colourtests =
 
 val _ = app colourpp_test colourtests
 
+fun good_oneline th =
+    null (hyp th) andalso
+    (let val cs = strip_conj (concl th)
+     in
+       length cs = 1 andalso is_eq (hd cs)
+     end)
+
+fun test msg th =
+    (tprint ("one_line_ify on " ^ msg);
+     require_msg (check_result good_oneline)
+                 (trace("assumptions", 1) thm_to_string)
+                 (DefnBase.one_line_ify NONE) th)
+val _ = test "cv_sub_def" cvTheory.cv_sub_def
+
 open groundEval numeralTheory
 
 val _ = overload_on ("B1", ``BIT1``);
@@ -124,3 +138,4 @@ val _ = testdot ``4 + 5 + 9`` ``18``;
 
 val _ = testdot ``(\x. x + y) 5`` ``5 + y``;
 val _ = testdot ``(\x. x + x + 1) ((\y. y + 10) 4)`` ``29``;
+