--- a/src/Pure/global_theory.ML Sat Jul 28 16:49:53 2018 +0200
+++ b/src/Pure/global_theory.ML Sat Jul 28 16:50:55 2018 +0200
@@ -158,7 +158,8 @@
end;
fun check_thms_lazy (thms: thm list lazy) =
- if Options.default_bool "strict_facts" then Lazy.force_value thms else thms;
+ if Proofterm.proofs_enabled () orelse Options.default_bool "strict_facts"
+ then Lazy.force_value thms else thms;
fun add_thms_lazy kind (b, thms) thy =
if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy