--- a/Quot/quotient_info.ML	Sat Dec 26 08:06:45 2009 +0100
+++ b/Quot/quotient_info.ML	Sat Dec 26 09:03:35 2009 +0100
@@ -13,7 +13,6 @@
   val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
   val quotdata_update_thy: string -> quotdata_info -> theory -> theory
   val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
-  val quotdata_dest: theory -> quotdata_info list
   val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}

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

--- a/Quot/quotient_typ.ML	Sat Dec 26 08:06:45 2009 +0100
+++ b/Quot/quotient_typ.ML	Sat Dec 26 09:03:35 2009 +0100
@@ -62,10 +62,7 @@
 fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
-     EVERY1 [rtac @{thm exI},
-             rtac mem_def2, 
-             rtac @{thm exI},
-             rtac @{thm refl}]
+     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
   Local_Theory.theory_result
     (Typedef.add_typedef false NONE
@@ -87,7 +84,7 @@
    RANGE [rtac equiv_thm,
           rtac rep_thm,
           rtac rep_inv,
-          EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}],
+          EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
           rtac rep_inj]) 1
 end
 
@@ -134,7 +131,7 @@
   val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
-  (* more abstract abs and rep definitions *)
+  (* more useful abs and rep definitions *)
   val abs_const = Const (@{const_name "Quot_Type.abs"}, dummyT )
   val rep_const = Const (@{const_name "Quot_Type.rep"}, dummyT )
   val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)