diff -r 2838109364f0 -r 98ec8b51af9c src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Nov 04 13:52:19 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Nov 04 17:19:33 2011 +0100
@@ -193,12 +193,13 @@
   end
 
 (* check for existence of map functions *)
-fun map_check ctxt (_, (rty, _, _)) =
+fun map_check thy (_, (rty, _, _)) =
   let
     fun map_check_aux rty warns =
       (case rty of
         Type (_, []) => warns
-      | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps ctxt s) then warns else s :: warns
+      | Type (s, _) =>
+          if is_some (Quotient_Info.lookup_quotmaps_global thy s) then warns else s :: warns
       | _ => warns)
 
     val warns = map_check_aux rty []
@@ -230,7 +231,7 @@
   let
     (* sanity check *)
     val _ = List.app sanity_check quot_list
-    val _ = List.app (map_check lthy) quot_list
+    val _ = List.app (map_check (Proof_Context.theory_of lthy)) quot_list
 
     fun mk_goal (rty, rel, partial) =
       let