# HG changeset patch
# User wenzelm
# Date 1703672496 -3600
# Node ID 18547955c942842d2cbf3e965011cf03841fb420
# Parent  b5853d438dbec86bf39cd64a745633cefe04ff45
tuned: avoid duplicates;

diff -r b5853d438dbe -r 18547955c942 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Wed Dec 27 11:14:56 2023 +0100
+++ b/src/Pure/global_theory.ML	Wed Dec 27 11:21:36 2023 +0100
@@ -306,10 +306,9 @@
     if name = "" then app_facts facts thy |-> register_proofs (name, pos)
     else
       let
-        val name_pos = Sign.bind_name thy b;
         val (thms', thy') = thy
-          |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
-          |>> name_thms name_flags2 name_pos |-> register_proofs (name, pos);
+          |> app_facts (map (apfst (name_thms name_flags1 (name, pos))) facts)
+          |>> name_thms name_flags2 (name, pos) |-> register_proofs (name, pos);
         val thy'' = thy' |> add_facts (b, Lazy.value thms');
       in (map (Thm.transfer thy'') thms', thy'') end
   end;