diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 36406fe57b..7d226b8108 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -48,7 +48,7 @@ instance : ToExpr (Fin n) where
   toExpr a :=
     let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
-      (mkApp2 (.const ``Fin.instOfNat []) (mkRawNatLit (n-1)) r)
+      (mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
 
 instance : ToExpr (BitVec n) where
   toTypeExpr := .app (mkConst ``BitVec) (toExpr n)