# HG changeset patch
# User kuncar
# Date 1332536417 -3600
# Node ID dfa5ed8d94b4edf591b0900940d993ab783ddecd
# Parent  e64ffc96a49f07089544f478960f1fc02637e218
use Thm.transfer for thms stored in generic context data storage

diff -r e64ffc96a49f -r dfa5ed8d94b4 src/HOL/Tools/Quotient/quotient_term.ML
--- 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})