| changeset 79113 | 5109e4b2a292 |
| parent 77979 | a12c48fbf10f |
| child 79278 | 8943cc46a66f |
--- a/src/Pure/global_theory.ML Fri Dec 01 18:12:18 2023 +0100 +++ b/src/Pure/global_theory.ML Sat Dec 02 15:42:50 2023 +0100 @@ -277,7 +277,7 @@ end; fun check_thms_lazy (thms: thm list lazy) = - if Proofterm.proofs_enabled () orelse Options.default_bool "strict_facts" + if Proofterm.any_proofs_enabled () orelse Options.default_bool "strict_facts" then Lazy.force_value thms else thms; fun add_thms_lazy kind (b, thms) thy =