From b37213e3786e806320752e320e255f8e8dbcca2a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 4 Dec 2020 18:11:53 -0800
Subject: [PATCH] chore: remove workaround

---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 9aa5494ed5..e79b854a1e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -452,7 +452,7 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do
       -- index 2 is unused.
       pure <| some (← descend ty 2 delab)
     else pure <| none
-  `(FIXME) -- `({ $[$fields, ]* $lastField $[: $ty]? })
+  `({ $[$fields, ]* $lastField $[: $ty]? })
 
 @[builtinDelab app.Prod.mk]
 def delabTuple : Delab := whenPPOption getPPNotation do