diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 3805b8c3d5..2147e50e7f 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -28,7 +28,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
         let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false)
         let fields : Array Syntax ← fields.mapM fun field => do
           let (isOptField, nm) := mkJsonField field
-          if isOptField then `($(mkIdent ``Json.opt) $nm (some $(mkIdent <| header.targetNames[0] ++ field)))
+          if isOptField then `(opt $nm (some $(mkIdent <| header.targetNames[0] ++ field)))
           else `([($nm, toJson $(mkIdent <| header.targetNames[0] ++ field))])
         let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* :=
           mkObj <| List.join [$fields,*])