merged

--- a/src/HOL/Quotient.thy	Sat Mar 24 12:28:45 2012 +0100
+++ b/src/HOL/Quotient.thy	Sat Mar 24 16:27:04 2012 +0100
@@ -960,4 +960,6 @@
   map_fun (infixr "--->" 55) and
   fun_rel (infixr "===>" 55)
 
+hide_const (open) invariant
+
 end

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 24 12:28:45 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 24 16:27:04 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})