# HG changeset patch
# User wenzelm
# Date 1524581980 -7200
# Node ID df9044efd0549860647c7eac228e2f8e5a595ea8
# Parent  1f9f973eed2a2801c15c35e6485c67e4c01f9d2f
eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);

diff -r 1f9f973eed2a -r df9044efd054 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Apr 24 14:17:58 2018 +0000
+++ b/src/Pure/Isar/locale.ML	Tue Apr 24 16:59:40 2018 +0200
@@ -420,7 +420,6 @@
 
 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)]));