tuned;
authorwenzelm
Sat Jul 28 16:30:58 2018 +0200 (11 months ago)
changeset 68699b624368a302f
parent 68698 6ee53660a911
child 68700 1e358063ab90
tuned;
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/global_theory.ML	Sat Jul 28 16:08:04 2018 +0200
     1.2 +++ b/src/Pure/global_theory.ML	Sat Jul 28 16:30:58 2018 +0200
     1.3 @@ -158,7 +158,7 @@
     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 thms; thms) else thms;
     1.8 +  if Options.default_bool "strict_facts" then Lazy.force_value thms else thms;
     1.9  
    1.10  fun add_thms_lazy kind (b, thms) thy =
    1.11    if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy