diff --git a/tests/lean/run/fingerprint.lean b/tests/lean/run/fingerprint.lean
index 5f0e9c41f3..218bb7a8f2 100644
--- a/tests/lean/run/fingerprint.lean
+++ b/tests/lean/run/fingerprint.lean
@@ -3,7 +3,7 @@ open tactic
 run_command attribute.fingerprint `reducible >>= trace
 
 definition ex0 : nat :=
-by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
+by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
 
 attribute [reducible]
 definition f : nat := 10
@@ -11,7 +11,7 @@ definition f : nat := 10
 run_command attribute.fingerprint `reducible >>= trace
 
 definition ex1 : nat :=
-by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
+by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
 
 vm_eval ex1
 
@@ -20,7 +20,7 @@ definition g : nat := 20
 run_command attribute.fingerprint `reducible >>= trace
 
 definition ex2 : nat :=
-by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
+by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
 
 vm_eval ex2
 
@@ -30,7 +30,7 @@ rfl
 definition h : nat := 20
 
 definition ex3 : nat :=
-by attribute.fingerprint `reducible >>= expr_of_nat >>= exact
+by attribute.fingerprint `reducible >>= nat.to_expr >>= exact
 
 example : ex1 = ex3 :=
 rfl
diff --git a/tests/lean/run/run_tactic1.lean b/tests/lean/run/run_tactic1.lean
index 5097cc26e0..75fd8e4f2e 100644
--- a/tests/lean/run/run_tactic1.lean
+++ b/tests/lean/run/run_tactic1.lean
@@ -15,7 +15,7 @@ meta definition mk_defs : nat → command
 | 0     := skip
 | (n+1) := do
    N ← to_expr `(nat),
-   v ← expr_of_nat n,
+   v ← n^.to_expr,
    add_decl (declaration.defn (name.append_after `val n) [] N v reducibility_hints.opaque tt),
    mk_defs n