# HG changeset patch
# User wenzelm
# Date 1703690305 -3600
# Node ID 6c12ef5bb38cb59e70d3fd43bebe316cb5e741b7
# Parent  589d8d9018d87948055877c50f8f5f20f241194a
tuned;

diff -r 589d8d9018d8 -r 6c12ef5bb38c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Dec 27 16:10:10 2023 +0100
+++ b/src/Pure/global_theory.ML	Wed Dec 27 16:18:25 2023 +0100
@@ -250,15 +250,16 @@
         |> (name <> "" andalso (post orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
 
+end;
+
+fun name_thm_flatten name_flags name =
+  name_thm name_flags (Thm_Name.flatten name);
+
 fun name_thms name_flags name_pos thms =
-  Thm_Name.list name_pos thms
-  |> map (fn (a, thm) => name_thm name_flags (Thm_Name.flatten a) thm);
+  Thm_Name.list name_pos thms |> map (uncurry (name_thm_flatten name_flags));
 
 fun name_facts name_flags name_pos facts =
-  Thm_Name.expr name_pos facts
-  |> (map o apfst o map) (fn (a, thm) => name_thm name_flags (Thm_Name.flatten a) thm);
-
-end;
+  Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm_flatten name_flags));
 
 
 (* store theorems and proofs *)