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