author | wenzelm |
Sat, 10 Mar 2018 15:52:47 +0100 | |
changeset 67814 | c4c4c2f01723 |
parent 67813 | 3e226d3b7bc6 |
child 67815 | 8b3d9a91706e |
--- 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)]));