# HG changeset patch
# User wenzelm
# Date 1571338569 -7200
# Node ID 15adbeb1fabdc4e0773a33055cce6d59408c5ae4
# Parent  ce1e27dcc9f4acb3a643dee65f93ba1cf02d7722
proper Thm.transfer;

diff -r ce1e27dcc9f4 -r 15adbeb1fabd src/Pure/global_theory.ML
--- 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;