1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20

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 ←