diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 566c00644..b55c21861 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1108,7 +1108,7 @@ class rewrite_fn {
                 r += t.pp(fmt);
             }
             format cs = pp_choice_symbols(m_lemma);
-            if (!cs.is_nil()) {
+            if (!cs.is_nil_fmt()) {
                 r += line() + format("rewrite lemma uses the following overloaded symbols");
                 r += nest(get_pp_indent(fmt.get_options()), line() + cs);
             }
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index 13a0280de..71d855e9d 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -224,7 +224,7 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n
     {
         sexpr list  = sexpr_compose_list(s);
         int len = 0;
-        while (list && !found_newline) {
+        while (!is_nil(list) && !found_newline) {
             sexpr const & h = car(list);
             list = cdr(list);
             len += space_upto_line_break(h, available, found_newline);
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index c151da9e1..82fa62be0 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -182,7 +182,7 @@ public:
     format_kind kind() const {
         return sexpr_kind(m_value);
     }
-    bool is_nil() const { return kind() == format_kind::NIL; }
+    bool is_nil_fmt() const { return kind() == format_kind::NIL; }
     unsigned hash() const { return m_value.hash(); }
 
     explicit operator bool() const { return static_cast<bool>(m_value); }