diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index bd81e50bd30ec55c386059807d44256633e355e6..5e315ca2fe9bcac6539cd5b89d9a6f5c81fda0f0 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -130,8 +130,8 @@ val solve_tac =
   \\ every_case_tac  \\ fs[]
   \\ `abs v <= abs (FST (widenInterval iv_e err_e)) \/
         abs v <= abs (SND (widenInterval iv_e err_e))`
-        by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
-  \\ TRY (every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
+        by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.OLD_REAL_ASM_ARITH_TAC)
+  \\ TRY (every_case_tac \\ RealArith.OLD_REAL_ASM_ARITH_TAC);
 
 Theorem FPRangeValidator_sound:
   ∀ e E1 E2 Gamma v m A fVars (dVars:num_set).