# HG changeset patch
# User wenzelm
# Date 1703413096 -3600
# Node ID 5071516d45a637addd867f6ab98c8d65b85c3df2
# Parent  13eb65caaffb54e55aea80cf2d5e2024c5e4ef64
tuned signature;

diff -r 13eb65caaffb -r 5071516d45a6 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Dec 24 11:13:54 2023 +0100
+++ b/src/Pure/global_theory.ML	Sun Dec 24 11:18:16 2023 +0100
@@ -26,6 +26,8 @@
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
+  val register_proofs_lazy: string * Position.T -> thm list lazy -> theory -> thm list lazy * theory
+  val register_proofs: string * Position.T -> thm list -> theory -> thm list * theory
   val name_multi: string * Position.T -> thm list -> ((string * Position.T) * thm) list
   type name_flags
   val unnamed: name_flags
@@ -212,6 +214,26 @@
 fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
 
 
+(* register 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_lazy (name, pos) (thms: thm list Lazy.lazy) thy =
+  let
+    val (thms', thy') =
+      if name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
+        fold_map (fn (a, th) => Thm.store_zproof (a, pos) th)
+          (Thm_Name.make_list name (Lazy.force thms)) thy
+        |>> Lazy.value
+      else (check_thms_lazy thms, thy);
+  in (thms', Thm.register_proofs thms' thy') end;
+
+fun register_proofs name thms =
+  register_proofs_lazy name (Lazy.value thms) #>> Lazy.force;
+
+
 (* name theorems *)
 
 fun name_multi (name, pos) =
@@ -245,24 +267,6 @@
 
 (* 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_lazy (name, pos) (thms: thm list Lazy.lazy) thy =
-  let
-    val (thms', thy') =
-      if name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
-        fold_map (fn (a, th) => Thm.store_zproof (a, pos) th)
-          (Thm_Name.make_list name (Lazy.force thms)) thy
-        |>> Lazy.value
-      else (check_thms_lazy thms, thy);
-  in (thms', Thm.register_proofs thms' thy') end;
-
-fun register_proofs name thms =
-  register_proofs_lazy name (Lazy.value thms) #>> Lazy.force;
-
-
 fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b);
 
 fun add_facts (b, fact) thy =