diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 151c90c85..be597a0d0 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1279,12 +1279,14 @@ public:
 
     void display_flyinfo(substitution const & s) {
         instantiate_flyinfo(s);
-        optional<flyinfo_data> prev;
+        flyinfo_data prev;
+        bool first = true;
         for (auto const & p : m_flyinfo_data) {
-            if (!prev || p.first != prev->first) {
+            if (first || p.first != prev.first) {
                 display_flyinfo_data(p);
                 prev = p;
             }
+            first = false;
         }
     }