diff -r 57944c1ef728 -r aa157e957655 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Dec 10 12:25:12 2009 +0100
+++ b/Quot/quotient_info.ML	Thu Dec 10 16:56:03 2009 +0100
@@ -6,14 +6,15 @@
   val maps_lookup: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
+  val print_mapsinfo: Proof.context -> unit
 
   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
-  val print_quotinfo: Proof.context -> unit
   val quotdata_lookup_thy: theory -> string -> quotient_info option
   val quotdata_lookup: Proof.context -> string -> quotient_info option
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
   val quotdata_dest: theory -> quotient_info list
+  val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
@@ -81,6 +82,25 @@
          (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
            "declaration of map information"))
 
+fun print_mapsinfo ctxt =
+let
+  fun prt_map (ty_name, {mapfun, relfun}) = 
+      Pretty.block (Library.separate (Pretty.brk 2)
+          [Pretty.str "type:", 
+           Pretty.str ty_name,
+           Pretty.str "map fun:", 
+           Pretty.str mapfun,
+           Pretty.str "relation map:", 
+           Pretty.str relfun])
+in
+  MapsData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map (prt_map)
+  |> Pretty.big_list "maps:" 
+  |> Pretty.writeln
+end
+
+
 
 (* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}