From 7a147eab12fb84abbc3edadb790853ad48b8fa06 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 29 Mar 2017 14:16:34 +0200
Subject: [PATCH] fix(frontends/lean/decl_util): truly fix top-level do pattern
 names race

---
 src/frontends/lean/decl_util.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 46ea0f1c03..6ab910e826 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -357,7 +357,7 @@ environment add_alias(environment const & env, bool is_protected, name const & c
 
 struct definition_info {
     name     m_prefix;
-    bool     m_is_private{false};
+    bool     m_is_private{true}; // pattern matching outside of definitions should generate private names
     bool     m_is_meta{false};
     bool     m_is_noncomputable{false};
     bool     m_is_lemma{false};