more robust: do not defer potentially slow/big lazy facts to the very end;
authorwenzelm
Sat Jul 28 16:50:55 2018 +0200 (11 months ago)
changeset 68701be936cf061ab
parent 68700 1e358063ab90
child 68702 8ef8905629ba
more robust: do not defer potentially slow/big lazy facts to the very end;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sat Jul 28 16:49:53 2018 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sat Jul 28 16:50:55 2018 +0200
     1.3 @@ -158,7 +158,8 @@
     1.4    end;
     1.5  
     1.6  fun check_thms_lazy (thms: thm list lazy) =
     1.7 -  if Options.default_bool "strict_facts" then Lazy.force_value thms else thms;
     1.8 +  if Proofterm.proofs_enabled () orelse Options.default_bool "strict_facts"
     1.9 +  then Lazy.force_value thms else thms;
    1.10  
    1.11  fun add_thms_lazy kind (b, thms) thy =
    1.12    if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy