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