# HG changeset patch
# User wenzelm
# Date 1703174495 -3600
# Node ID a6d9631662c7df5ba1a0414ddae8e219774e31f9
# Parent  8a292105351116775b49f16e399c43613bc66559
tuned;

diff -r 8a2921053511 -r a6d9631662c7 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Dec 21 11:58:19 2023 +0100
+++ b/src/Pure/global_theory.ML	Thu Dec 21 17:01:35 2023 +0100
@@ -245,6 +245,10 @@
 
 (* store theorems and proofs *)
 
+fun check_thms_lazy (thms: thm list lazy) =
+  if Proofterm.any_proofs_enabled () orelse Options.default_bool "strict_facts"
+  then Lazy.force_value thms else thms;
+
 fun register_proofs thms thy =
   let
     val (thms', thy') =
@@ -282,10 +286,6 @@
     thy |> map_facts (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
   end;
 
-fun check_thms_lazy (thms: thm list lazy) =
-  if Proofterm.any_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
   else