diff -r fb4bfbb1a291 -r a31cf260eeb3 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Dec 26 08:06:45 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 26 09:03:35 2009 +0100
@@ -209,20 +209,37 @@
 *)
 
 (* instantiates TVars so that the term is of type ty *)
-fun force_typ thy trm ty =
+fun force_typ ctxt trm ty =
 let
+  val thy = ProofContext.theory_of ctxt 
   val trm_ty = fastype_of trm
   val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
 in
   map_types (Envir.subst_type ty_inst) trm
 end
 
+fun get_relmap ctxt s =
+let
+  val thy = ProofContext.theory_of ctxt
+  val exc =  LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") 
+  val relmap =  #relmap (maps_lookup thy s) handle NotFound => raise exc
+in
+  Const (relmap, dummyT)
+end
+
+fun get_equiv_rel ctxt s =
+let
+  val thy = ProofContext.theory_of ctxt
+  val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") 
+in
+  #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc
+end
+
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
+
+(* FIXME: check that the types correspond to each other? *)
 fun mk_resp_arg ctxt (rty, qty) =
-let
-  val thy = ProofContext.theory_of ctxt
-in  
   if rty = qty
   then HOLogic.eq_const rty
   else
@@ -231,29 +248,18 @@
        if s = s' 
        then 
          let
-           val exc = LIFT_MATCH ("mk_resp_arg (no relation 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 (relmap, dummyT), args) 
+           list_comb (get_relmap ctxt s, args) 
          end  
        else 
          let
-           val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") 
-           val equiv_rel = #equiv_rel (quotdata_lookup 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_equiv_rel = force_typ thy equiv_rel (rty --> rty --> @{typ bool})
+           val eqv_rel = get_equiv_rel ctxt s'
          in
-           forced_equiv_rel
+           force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          end
       | _ => HOLogic.eq_const rty
-             (* FIXME: check that the types correspond to each other? *)
-end
-
+            
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)