src/Pure/pure_thy.ML
changeset 9007 135c998d2b46
parent 8720 840c75ab2a7f
child 9192 df32cd0881b9
--- a/src/Pure/pure_thy.ML	Wed May 31 14:14:59 2000 +0200
+++ b/src/Pure/pure_thy.ML	Wed May 31 14:26:46 2000 +0200
@@ -122,7 +122,7 @@
 fun get_thms thy name =
   (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of
     None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
-  | Some thms => thms);
+  | Some thms => map (Thm.transfer thy) thms);
 
 fun get_thm thy name =
   (case get_thms thy name of