diff --git a/src/num/theories/cv_compute/selftest.sml b/src/num/theories/cv_compute/selftest.sml
index 40367ca561..6478c9333a 100644
--- a/src/num/theories/cv_compute/selftest.sml
+++ b/src/num/theories/cv_compute/selftest.sml
@@ -6,14 +6,14 @@ fun simp ths = simpLib.ASM_SIMP_TAC (BasicProvers.srw_ss()) ths
 val M = “(λf n. cv_if (cv_lt n (cv$Num 1)) (cv$Num 1)
              (cv_mul n (f (cv_sub n (cv$Num 1)))))”
 val factc_def0 = new_definition("factc_def0",
-  “factc = WFREC (measure cv_size_alt) ^M”);
+  “factc = WFREC (measure cv_size) ^M”);
 
 val restrict_lemma = Q.prove(
-  ‘^M (RESTRICT factc (measure cv_size_alt) x) x = ^M factc x’,
+  ‘^M (RESTRICT factc (measure cv_size) x) x = ^M factc x’,
   BETA_TAC >> irule cv_if_cong >> simp[] >>
   Q.SPEC_THEN ‘x’ STRUCT_CASES_TAC (TypeBase.nchotomy_of “:cv”) >>
   simp[] >> IF_CASES_TAC >> simp[c2b_def] >>
-  simp[relationTheory.RESTRICT_DEF, cv_size_alt_def] >>
+  simp[relationTheory.RESTRICT_DEF, cv_size_def] >>
   Q.RENAME_TAC [‘n <> 0’] >>
   reverse $ Q.SUBGOAL_THEN ‘n - 1 < n’ ASSUME_TAC >- simp[] >>
   irule SUB_LESS >> pop_assum mp_tac >>
@@ -21,7 +21,7 @@ val restrict_lemma = Q.prove(
   simp[ONE, LESS_EQ_MONO, ZERO_LESS_EQ]);
 
 val factc_def = MATCH_MP relationTheory.WFREC_THM
-                         (Q.ISPEC ‘cv_size_alt’ prim_recTheory.WF_measure)
+                         (Q.ISPEC ‘cv_size’ prim_recTheory.WF_measure)
                          |> ISPEC M
                          |> REWRITE_RULE[restrict_lemma, GSYM factc_def0]
                          |> BETA_RULE