diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp
index e5a91fb19f..3a3e369e11 100644
--- a/src/frontends/lean/parser_config.cpp
+++ b/src/frontends/lean/parser_config.cpp
@@ -202,9 +202,11 @@ transition read_transition(deserializer & d) {
     return transition(n, a, pp);
 }
 
+struct notation_prio_fn { unsigned operator()(notation_entry const & v) const { return v.priority(); } };
+
 struct notation_state {
     typedef rb_map<mpz, list<expr>, mpz_cmp_fn> num_map;
-    typedef head_map<notation_entry>            head_to_entries;
+    typedef head_map_prio<notation_entry, notation_prio_fn> head_to_entries;
     parse_table      m_nud;
     parse_table      m_led;
     num_map          m_num_map;
diff --git a/tests/lean/notation_pp_priority.lean b/tests/lean/notation_pp_priority.lean
new file mode 100644
index 0000000000..3ffa212099
--- /dev/null
+++ b/tests/lean/notation_pp_priority.lean
@@ -0,0 +1,28 @@
+prelude
+
+import init.data.nat.basic
+
+noncomputable theory
+
+constant some_type : Type
+constants foo bar : some_type
+
+/-
+  Test that notation with a high priority is used by the pretty-printer,
+  regardless of the order in which they are declared.
+-/
+section
+  notation [priority 2000] `high_before_low` := foo
+  notation [priority 1] `low_after_high` := foo
+
+  def test_high_before_low := foo
+  #print test_high_before_low
+end
+
+section
+  notation [priority 1] `low_before_high` := bar
+  notation [priority 2000] `high_after_low` := bar
+
+  def test_high_after_low := bar
+  #print test_high_after_low
+end
diff --git a/tests/lean/notation_pp_priority.lean.expected.out b/tests/lean/notation_pp_priority.lean.expected.out
new file mode 100644
index 0000000000..25ec306096
--- /dev/null
+++ b/tests/lean/notation_pp_priority.lean.expected.out
@@ -0,0 +1,4 @@
+noncomputable def test_high_before_low : some_type :=
+high_before_low
+noncomputable def test_high_after_low : some_type :=
+high_after_low