# HG changeset patch
# User wenzelm
# Date 1532789455 -7200
# Node ID be936cf061abb82376cdfef71560cb1829b4f0c8
# Parent  1e358063ab9005a20c619ddba197280a22cde36b
more robust: do not defer potentially slow/big lazy facts to the very end;

diff -r 1e358063ab90 -r be936cf061ab src/Pure/global_theory.ML
--- 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