diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean
index 1fa2a5e2d7be..382b5fe45a8f 100644
--- a/src/lake/Lake/CLI/Translate/Lean.lean
+++ b/src/lake/Lake/CLI/Translate/Lean.lean
@@ -141,7 +141,7 @@ instance : ToLean Backend := ⟨Backend.toLean⟩
 def quoteLeanOptionValue : LeanOptionValue → Term
 | .ofString v => toLean v
 | .ofBool v => toLean v
-| .ofNat v => toLean v
+| .ofNat v => Unhygienic.run `(.ofNat $(toLean v))
 
 instance : ToLean LeanOptionValue := ⟨quoteLeanOptionValue⟩