--- a/Quot/quotient_info.ML	Wed Dec 23 22:42:30 2009 +0100
+++ b/Quot/quotient_info.ML	Wed Dec 23 23:22:02 2009 +0100
@@ -2,15 +2,15 @@
 sig
   exception NotFound
 
-  type maps_info = {mapfun: string, relfun: string}
-  val maps_lookup: theory -> string -> maps_info       (* raises NotFound *)
+  type maps_info = {mapfun: string, relmap: string}
+  val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
   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 quotdata_lookup_thy: theory -> string -> quotient_info option
-  val quotdata_lookup: Proof.context -> string -> quotient_info option
+  type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+  val quotdata_lookup_thy: theory -> string -> quotient_info     (* raises NotFound *)
+  val quotdata_lookup: Proof.context -> string -> quotient_info     (* raises NotFound *)
   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
@@ -18,7 +18,7 @@
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
-  val qconsts_lookup: theory -> term -> qconsts_info    (* raises NotFound *)
+  val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
   val qconsts_dest: theory -> qconsts_info list
@@ -43,7 +43,7 @@
 (*******************)
 
 (* info about map- and rel-functions for a type *)
-type maps_info = {mapfun: string, relfun: string}
+type maps_info = {mapfun: string, relmap: string}
 
 structure MapsData = Theory_Data
   (type T = maps_info Symtab.table
@@ -73,7 +73,7 @@
   fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
   val _ =  map sanity_check [mapname, relname]
 in
-  maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
+  maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
 end
 
 val maps_attr_parser = 
@@ -88,12 +88,12 @@
 
 fun print_mapsinfo ctxt =
 let
-  fun prt_map (ty_name, {mapfun, relfun}) = 
+  fun prt_map (ty_name, {mapfun, relmap}) = 
       Pretty.block (Library.separate (Pretty.brk 2)
         (map Pretty.str 
           ["type:", ty_name,
-           "map fun:", mapfun,
-           "relation map:", relfun]))
+           "map:", mapfun,
+           "relation map:", relmap]))
 in
   MapsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
@@ -104,7 +104,7 @@
 
  
 (* info about quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
+type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
 
 structure QuotData = Theory_Data
   (type T = quotient_info Symtab.table
@@ -112,13 +112,19 @@
    val extend = I
    val merge = Symtab.merge (K true)) 
 
-fun quotdata_lookup_thy thy str = 
-    Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
+fun quotdata_lookup_thy thy s = 
+  case Symtab.lookup (QuotData.get thy) (Sign.intern_type thy s) of
+    SOME qinfo => qinfo
+  | NONE => raise NotFound
 
 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
-fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
-      QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
+fun quotdata_update_thy qty_name (qty, rty, equiv_rel, equiv_thm) =
+let
+  val qinfo = {qtyp = qty, rtyp = rty, equiv_rel = equiv_rel, equiv_thm = equiv_thm}
+in
+  QuotData.map (Symtab.update (qty_name, qinfo))
+end
 
 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
@@ -128,14 +134,14 @@
 
 fun print_quotinfo ctxt =
 let
-  fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
+  fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = 
       Pretty.block (Library.separate (Pretty.brk 2)
           [Pretty.str "quotient type:", 
            Syntax.pretty_typ ctxt qtyp,
            Pretty.str "raw type:", 
            Syntax.pretty_typ ctxt rtyp,
            Pretty.str "relation:", 
-           Syntax.pretty_term ctxt rel,
+           Syntax.pretty_term ctxt equiv_rel,
            Pretty.str "equiv. thm:", 
            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in