more robust: do not defer potentially slow/big lazy facts to the very end;

--- 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