get_thm(s): automatic transfer;

--- a/src/Pure/Isar/proof_context.ML	Wed May 31 14:14:59 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed May 31 14:26:46 2000 +0200
@@ -814,13 +814,13 @@
 
 fun get_thm (ctxt as Context {thy, thms, ...}) name =
   (case Symtab.lookup (thms, name) of
-    Some (Some [th]) => th
+    Some (Some [th]) => Thm.transfer thy th
   | Some (Some _) => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
   | _ => (PureThy.get_thm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
 
 fun get_thms (ctxt as Context {thy, thms, ...}) name =
   (case Symtab.lookup (thms, name) of
-    Some (Some ths) => ths
+    Some (Some ths) => map (Thm.transfer thy) ths
   | _ => (PureThy.get_thms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
 
 fun get_thmss ctxt names = flat (map (get_thms ctxt) names);

--- 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