diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 872f2d3164..e647588be8 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -798,7 +798,7 @@ local
         handle Feedback.HOL_ERR _ =>
 
         if term_contains_real_ty t then
-          profile "rewrite(11.1)(REAL_ARITH)" RealArith.REAL_ARITH t
+          profile "rewrite(11.1)(REAL_ARITH)" RealField.REAL_ARITH t
         else
           profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t
     in
@@ -836,7 +836,7 @@ local
           (* this is just a heuristic - it is quite conceivable that a
              term that contains type real is provable by integer
              arithmetic *)
-          profile "th_lemma[arith](3.1)(real)" RealArith.REAL_ARITH t'
+          profile "th_lemma[arith](3.1)(real)" RealField.REAL_ARITH t'
         else
           profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t'
       val subst = List.map (fn (term, var) => {redex = var, residue = term})
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 8841a4a104..1cebbf5813 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -213,9 +213,6 @@ in
 
     (* real *)
 
-    (* Z3 2.19 prints reals as integers in its proofs; I see no way to
-       reliably distinguish between them. *)
-
     (``0r = 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``1r = 1r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``0r = 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -450,9 +447,9 @@ in
     (``1 * (x:real) = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``(x:real) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (``abs (x:real) >= 0``, [thm_AUTO, thm_YO]),
     (``(abs (x:real) = 0) = (x = 0)``, [thm_AUTO, thm_YO]),
@@ -551,10 +548,10 @@ in
     (``(x:real) < x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:real) < y ==> 42 * x < 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``0n <= 1n``, [thm_AUTO, thm_YO]),
-    (``1n <= 0n``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:num) <= x``, [thm_AUTO, thm_YO]),
-    (``(x:num) <= y ==> 2 * x <= 2 * y``, [thm_AUTO, thm_YO]),
+    (``0r <= 1r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``1r <= 0r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
+    (``(x:real) <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:real) <= y ==> 42 * x <= 42 * y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (``1r > 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``0r > 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),