src/Pure/ROOT.ML
changeset 59714 ae322325adbb
parent 59470 31d810570879
child 59901 840d03805755
--- a/src/Pure/ROOT.ML	Mon Mar 16 11:07:56 2015 +0100
+++ b/src/Pure/ROOT.ML	Mon Mar 16 11:30:54 2015 +0100
@@ -310,6 +310,7 @@
 use "PIDE/resources.ML";
 use "Thy/thy_info.ML";
 use "PIDE/session.ML";
+use "PIDE/protocol_message.ML";
 use "PIDE/document.ML";
 
 (*theory and proof operations*)