author | wenzelm |
Sat, 28 Jul 2018 16:30:58 +0200 | |
changeset 68699 | b624368a302f |
parent 68698 | 6ee53660a911 |
child 68700 | 1e358063ab90 |
--- a/src/Pure/global_theory.ML Sat Jul 28 16:08:04 2018 +0200 +++ b/src/Pure/global_theory.ML Sat Jul 28 16:30:58 2018 +0200 @@ -158,7 +158,7 @@ end; fun check_thms_lazy (thms: thm list lazy) = - if Options.default_bool "strict_facts" then (Lazy.force thms; thms) else thms; + if 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