diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index f070cc5f2a..3686f19109 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1842,7 +1842,7 @@ std::string sexpr_to_string(sexpr const & s) {
 // check whether a space must be inserted between the strings so that lexing them would
 // produce separate tokens
 std::pair<bool, token_table const *> pretty_fn::needs_space_sep(token_table const * last, std::string const & s1, std::string const & s2) const {
-    if (is_id_rest(get_utf8_last_char(s1.data()), s1.data() + s1.size()) && is_id_rest(s2.data(), s2.data() + s2.size()))
+    if (s1.size() == 0 || (is_id_rest(get_utf8_last_char(s1.data()), s1.data() + s1.size()) && is_id_rest(s2.data(), s2.data() + s2.size())))
         return mk_pair(true, nullptr); // would be lexed as a single identifier without space
 
     if (last) {
diff --git a/src/util/name.cpp b/src/util/name.cpp
index b37c68012b..bb6d884405 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -75,7 +75,7 @@ void name::imp::display_core(std::ostream & out, imp * p, bool escape, char cons
                 }
             }
         }
-        if (must_escape)
+        if (must_escape || sz == 0)
             out << "«" << p->m_str << "»";
         else
             out << p->m_str;
diff --git a/tests/lean/empty_french_quote.lean b/tests/lean/empty_french_quote.lean
new file mode 100644
index 0000000000..35201c4e90
--- /dev/null
+++ b/tests/lean/empty_french_quote.lean
@@ -0,0 +1,4 @@
+def «» := not
+theorem thm : «» false := id
+#print «»
+#print thm
\ No newline at end of file
diff --git a/tests/lean/empty_french_quote.lean.expected.out b/tests/lean/empty_french_quote.lean.expected.out
new file mode 100644
index 0000000000..35fff6084a
--- /dev/null
+++ b/tests/lean/empty_french_quote.lean.expected.out
@@ -0,0 +1,4 @@
+def «» : Prop → Prop :=
+not
+theorem thm : «» false :=
+id