diff --git a/src/Init/Lean/Linter.lean b/src/Init/Lean/Linter.lean
index e2535572ca..2a1c51e64e 100644
--- a/src/Init/Lean/Linter.lean
+++ b/src/Init/Lean/Linter.lean
@@ -7,7 +7,7 @@ prelude
 import Init.System.IO
 import Init.Lean.Attributes
 import Init.Lean.Syntax
-import Init.Lean.Util.Message
+import Init.Lean.Message
 
 namespace Lean
 
diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Message.lean
similarity index 100%
rename from src/Init/Lean/Util/Message.lean
rename to src/Init/Lean/Message.lean
diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean
index bc739fe88b..09c3a158ad 100644
--- a/src/Init/Lean/Meta/Exception.lean
+++ b/src/Init/Lean/Meta/Exception.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Lean.Environment
 import Init.Lean.MetavarContext
-import Init.Lean.Util.Message
+import Init.Lean.Message
 
 namespace Lean
 namespace Meta
diff --git a/src/Init/Lean/Parser/Module.lean b/src/Init/Lean/Parser/Module.lean
index f958cc8302..fda6197cf1 100644
--- a/src/Init/Lean/Parser/Module.lean
+++ b/src/Init/Lean/Parser/Module.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import Init.Lean.Util.Message
+import Init.Lean.Message
 import Init.Lean.Parser.Command
 
 namespace Lean
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index c46ccf1cc3..bd8bb126c0 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -10,7 +10,7 @@ import Init.Lean.Syntax
 import Init.Lean.ToExpr
 import Init.Lean.Environment
 import Init.Lean.Attributes
-import Init.Lean.Util.Message
+import Init.Lean.Message
 import Init.Lean.Parser.Identifier
 import Init.Lean.Compiler.InitAttr
 
diff --git a/src/Init/Lean/Util/Sorry.lean b/src/Init/Lean/Util/Sorry.lean
index c3e8300d2f..2cb9764e3f 100644
--- a/src/Init/Lean/Util/Sorry.lean
+++ b/src/Init/Lean/Util/Sorry.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Util.Message
+import Init.Lean.Message
 
 namespace Lean
 
diff --git a/src/Init/Lean/Util/Trace.lean b/src/Init/Lean/Util/Trace.lean
index f08ed718c5..055d087fb6 100644
--- a/src/Init/Lean/Util/Trace.lean
+++ b/src/Init/Lean/Util/Trace.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
-import Init.Lean.Util.Message
+import Init.Lean.Message
 universe u
 
 namespace Lean