diff -r a5495a323b49 -r 90bde96f5dd1 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Jan 05 14:09:04 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 05 14:23:45 2010 +0100
@@ -249,10 +249,17 @@
   #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc
 end
 
+fun equiv_match_err ctxt ty_pat ty =
+let
+  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+  val ty_str = Syntax.string_of_typ ctxt ty 
+in
+  raise LIFT_MATCH (space_implode " " 
+    ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+end
+
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
-
-(* FIXME: check that the types correspond to each other *)
 fun new_equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty
@@ -271,9 +278,9 @@
            val thy = ProofContext.theory_of ctxt
            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
            val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
-                        handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
+                        handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty
            val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
-                        handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty 
+                        handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty 
            val args_aux = map (double_lookup rtyenv qtyenv) vs 
            val args = map (new_equiv_relation ctxt) args_aux
            val rel_map = mk_relmap ctxt vs rty_pat