diff --git a/src/kernel/pos_info_provider.h b/src/kernel/pos_info_provider.h
index 5b3fa3b7b3..2055677e10 100644
--- a/src/kernel/pos_info_provider.h
+++ b/src/kernel/pos_info_provider.h
@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/sexpr/format.h"
 #include "kernel/expr.h"
+#include "util/message_definitions.h"
 
 namespace lean {
-typedef pair<unsigned, unsigned> pos_info; //!< Line and column information
 /**
    \brief Abstract class for providing expression position information (line number and column).
 */
diff --git a/src/library/message_buffer.h b/src/library/message_buffer.h
index 8bfdf11965..bc5c97ed8b 100644
--- a/src/library/message_buffer.h
+++ b/src/library/message_buffer.h
@@ -11,16 +11,10 @@ Author: Gabriel Ebner
 #include "util/exception.h"
 #include "util/name_set.h"
 #include "library/messages.h"
+#include "util/message_definitions.h"
 
 namespace lean {
 
-typedef uint64 period;
-
-struct message_bucket_id {
-    name m_bucket;
-    period m_version;
-};
-
 class info_manager;
 
 class message_buffer {
diff --git a/src/library/mt_task_queue.h b/src/library/mt_task_queue.h
index d2b5f75103..9657c5ab99 100644
--- a/src/library/mt_task_queue.h
+++ b/src/library/mt_task_queue.h
@@ -15,6 +15,7 @@ Author: Gabriel Ebner
 #include "util/optional.h"
 #include "library/io_state.h"
 #include "library/task_queue.h"
+#include "library/message_buffer.h"
 
 namespace lean {
 
diff --git a/src/library/task_helper.cpp b/src/library/task_helper.cpp
index 2ed6066978..ffed25bf2a 100644
--- a/src/library/task_helper.cpp
+++ b/src/library/task_helper.cpp
@@ -5,9 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 */
 #include <string>
-#include <library/trace.h>
-#include <library/message_builder.h>
+#include "library/trace.h"
+#include "library/message_builder.h"
 #include "library/task_helper.h"
+#include "library/message_buffer.h"
 
 namespace lean {
 
diff --git a/src/library/task_queue.cpp b/src/library/task_queue.cpp
index 4e2124f8be..7dd750e2ff 100644
--- a/src/library/task_queue.cpp
+++ b/src/library/task_queue.cpp
@@ -6,6 +6,7 @@ Author: Gabriel Ebner
 */
 #include <string>
 #include "library/task_queue.h"
+#include "library/message_buffer.h"
 
 namespace lean {
 
diff --git a/src/library/task_queue.h b/src/library/task_queue.h
index a85c3256a3..2b7f94806f 100644
--- a/src/library/task_queue.h
+++ b/src/library/task_queue.h
@@ -12,7 +12,7 @@ Author: Gabriel Ebner
 #include "util/thread.h"
 #include "util/optional.h"
 #include "util/rc.h"
-#include "library/message_buffer.h"
+#include "util/message_definitions.h"
 
 namespace lean {
 
diff --git a/src/util/message_definitions.h b/src/util/message_definitions.h
new file mode 100644
index 0000000000..f44a206474
--- /dev/null
+++ b/src/util/message_definitions.h
@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Gabriel Ebner
+*/
+#pragma once
+#include <utility>
+#include "util/name.h"
+#include "util/int64.h"
+
+namespace lean {
+
+typedef pair<unsigned, unsigned> pos_info; //!< Line and column information
+
+typedef uint64 period;
+
+struct message_bucket_id {
+    name m_bucket;
+    period m_version;
+};
+
+}