proper transfer for Thm.derivation_name;
authorwenzelm
Thu, 12 Mar 2020 20:58:18 +0100
changeset 71753 c983fd846c9c
parent 71752 138e8226961e
child 71754 3cad8ffee92c
proper transfer for Thm.derivation_name;
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