diff --git a/Lens/Elab.lean b/Lens/Elab.lean
index 9d9c1bc..98a708d 100644
--- a/Lens/Elab.lean
+++ b/Lens/Elab.lean
@@ -21,12 +21,9 @@ elab "makeLenses" structIdent:ident : command => do
     let fieldNameIdent := mkIdent field.fieldName
     let some decl := env.find? (field.projFn)
       | throwErrorAt structIdent s!"Could not find project function {field.projFn}"
-    let (some fieldTypeName, some fieldTypeArgs) := (← liftTermElabM (liftMetaM (
-             forallTelescope decl.type fun _ body
-               => pure (body.getAppFn.constName?, body.getAppArgs.mapM (·.constName?)))))
-      | throwErrorAt structIdent "Not a structure name"
-    let d ← fieldTypeArgs.mapM fun argName => `($(mkIdent argName))
-    let fieldTypeNameIdent := Syntax.mkCApp fieldTypeName d
+    let fieldTypeNameIdent : Term ← liftTermElabM <| liftMetaM <|
+      forallTelescope decl.type fun _ body =>
+        Lean.PrettyPrinter.delab body
     let lensName := mkIdent field.fieldName
     let newVal := mkIdent <| Name.mkSimple "newVal"
     let l ←
diff --git a/lean-toolchain b/lean-toolchain
index 4c685fa..af9e5d3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.28.0
+leanprover/lean4:v4.30.0