author | wenzelm |
Tue, 24 Apr 2018 16:59:40 +0200 | |
changeset 68029 | df9044efd054 |
parent 68028 | 1f9f973eed2a |
child 68030 | 0a6d6ba383dc |
--- 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)]));