# HG changeset patch
# User wenzelm
# Date 968877135 -7200
# Node ID 035a8288310a9ed88ea4675239202440ed543310
# Parent  24914e42b857bd5600d29cd39d152ec326752c10
begin_theory: priority message to gain some robustness in sync communication;

diff -r 24914e42b857 -r 035a8288310a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Sep 13 22:31:19 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Sep 13 22:32:15 2000 +0200
@@ -385,6 +385,7 @@
   let
     val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
     val _ = check_unfinished error name;
+    val _ = priority (loader_msg "looking up" [name]);
     val _ = (map Path.basic parents; seq assert_thy parents);
     val theory = PureThy.begin_theory name (map get_theory parents);
     val deps =