--- a/Quot/quotient_term.ML	Wed Dec 23 22:42:30 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 23:22:02 2009 +0100
@@ -45,9 +45,9 @@
 let
   val thy = ProofContext.theory_of ctxt
   val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])
-  val info = maps_lookup thy ty_str handle NotFound => raise exc
+  val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc
 in
-  Const (#mapfun info, dummyT)
+  Const (mapfun, dummyT)
 end
 
 fun get_absrep_const flag ctxt _ qty =
@@ -145,23 +145,24 @@
        if s = s' 
        then 
          let
-           val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) 
-           val map_info = maps_lookup thy s handle NotFound => raise exc
+           val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") 
+           val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc
            val args = map (mk_resp_arg ctxt) (tys ~~ tys')
          in
-           list_comb (Const (#relfun map_info, dummyT), args) 
+           list_comb (Const (relmap, dummyT), args) 
          end  
        else 
-         let  
-           val SOME qinfo = quotdata_lookup_thy thy s'
+         let
+           val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") 
+           val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc
            (* FIXME: check in this case that the rty and qty *)
            (* FIXME: correspond to each other *)
 
            (* we need to instantiate the TVars in the relation *)
            val thy = ProofContext.theory_of ctxt 
-           val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool})
+           val forced_equiv_rel = force_typ thy equiv_rel (rty --> rty --> @{typ bool})
          in
-           forced_rel
+           forced_equiv_rel
          end
       | _ => HOLogic.eq_const rty
              (* FIXME: check that the types correspond to each other? *)