use Thm.transfer for thms stored in generic context data storage

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 18:23:47 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 22:00:17 2012 +0100
@@ -336,19 +336,25 @@
 
 (* generation of the Quotient theorem  *)
 
+exception CODE_GEN of string
+
 fun get_quot_thm ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt
   in
-    (case Quotient_Info.lookup_quotients_global thy s of
-      SOME qdata => #quot_thm qdata
-    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+    (case Quotient_Info.lookup_quotients ctxt s of
+      SOME qdata => Thm.transfer thy (#quot_thm qdata)
+    | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
   end
 
-fun get_rel_quot_thm thy s =
-  (case Quotient_Info.lookup_quotmaps thy s of
-    SOME map_data => #quot_thm map_data
-  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
+fun get_rel_quot_thm ctxt s =
+   let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    (case Quotient_Info.lookup_quotmaps ctxt s of
+      SOME map_data => Thm.transfer thy (#quot_thm map_data)
+    | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
+  end
 
 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})