# HG changeset patch
# User wenzelm
# Date 1584043098 -3600
# Node ID c983fd846c9c77e82d02e2555e4c9aaed607a5b2
# Parent  138e8226961e1011b2c2616f6bb9d52039684477
proper transfer for Thm.derivation_name;

diff -r 138e8226961e -r c983fd846c9c src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Tue Mar 10 22:52:21 2020 +0100
+++ b/src/Pure/thm_deps.ML	Thu Mar 12 20:58:18 2020 +0100
@@ -87,10 +87,10 @@
       if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I
       else
         let val {concealed, group, ...} = Name_Space.the_entry space name in
-          fold_rev (fn th =>
+          fold_rev (transfer #> (fn th =>
             (case Thm.derivation_name th of
               "" => I
-            | a => cons (a, (transfer th, concealed, group)))) ths
+            | a => cons (a, (th, concealed, group))))) ths
         end;
     fun add_facts thy =
       let