# HG changeset patch
# User wenzelm
# Date 1703705461 -3600
# Node ID 06ab0a304f29e2eaac04c00cfae170266a81aa67
# Parent  6c12ef5bb38cb59e70d3fd43bebe316cb5e741b7
tuned;
more uniform Thm.transfer;

diff -r 6c12ef5bb38c -r 06ab0a304f29 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Dec 27 16:18:25 2023 +0100
+++ b/src/Pure/global_theory.ML	Wed Dec 27 20:31:01 2023 +0100
@@ -303,31 +303,28 @@
 
 (* apply theorems and attributes *)
 
-local
-
-val app_facts =
-  fold_maps (fn (thms, atts) => fn thy =>
-    fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
-
-in
-
 fun apply_facts zproof name_flags1 name_flags2 (b, facts) thy =
   let
     val name = Sign.full_name_pos thy b;
+    val named_facts = Thm_Name.expr name facts;
+
+    val unnamed = #1 name = "";
+    val name_thm1 = if unnamed then #2 else uncurry (name_thm_flatten name_flags1);
+
+    val app_facts =
+      fold_maps (fn (named_thms, atts) => fn thy =>
+        let val thms = map name_thm1 named_thms
+        in fold_map (Thm.theory_attributes atts o Thm.transfer thy) thms thy end);
     val register = register_proofs zproof name;
   in
-    if #1 name = "" then app_facts facts thy |-> register
+    if unnamed then app_facts named_facts thy |-> register
     else
       let
-        val (thms', thy') = thy
-          |> app_facts (name_facts name_flags1 name facts)
-          |>> name_thms name_flags2 name |-> register;
+        val (thms', thy') = app_facts named_facts thy |>> name_thms name_flags2 name |-> register;
         val thy'' = thy' |> add_facts (b, Lazy.value thms');
       in (map (Thm.transfer thy'') thms', thy'') end
   end;
 
-end;
-
 
 (* store_thm *)