# HG changeset patch
# User wenzelm
# Date 1520693567 -3600
# Node ID c4c4c2f01723453c33435ad2211ceb249523d4c3
# Parent  3e226d3b7bc69241765e11c54819341c254fc674
workaround for occasional deadlock seen in HOL-Proofs with threads=2;

diff -r 3e226d3b7bc6 -r c4c4c2f01723 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 10 14:43:15 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 10 15:52:47 2018 +0100
@@ -420,6 +420,7 @@
 
 fun make_notes kind = map (fn ((b, atts), facts) =>
   if null atts andalso forall (null o #2) facts
+    andalso not (Proofterm.proofs_enabled ()) (* FIXME *)
   then Lazy_Notes (kind, (b, Lazy.value (maps #1 facts)))
   else Notes (kind, [((b, atts), facts)]));