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