proper Thm.transfer;

--- a/src/Pure/global_theory.ML	Thu Oct 17 20:28:31 2019 +0200
+++ b/src/Pure/global_theory.ML	Thu Oct 17 20:56:09 2019 +0200
@@ -187,6 +187,7 @@
     | (SOME {thms, ...}, _) =>
         if i > 0 andalso i <= length thms then nth thms (i - 1)
         else Facts.err_selection (print_name (), pos) i thms)
+    |> Thm.transfer thy
   end;