diff -r 999870716cc8 -r 5c6d76c3ba5c Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 13 16:14:02 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 13 16:23:32 2010 +0100
@@ -373,6 +373,17 @@
     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
   | _ => f (trm1, trm2)
 
+fun relation_error ctxt r1 r2 =
+let
+  val r1s = Syntax.string_of_term ctxt r1
+  val r2s = Syntax.string_of_term ctxt r2
+  val r1t = Syntax.string_of_typ ctxt (fastype_of r1)
+  val r2t = Syntax.string_of_typ ctxt (fastype_of r2)
+in
+  raise LIFT_MATCH ("regularise (relation mismatch)\n[" ^
+  r1s ^ " :: " ^ r1t ^ "]\n[" ^ r2s ^ " :: " ^ r2t ^ "]")
+end
+
 (* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)
 
@@ -416,18 +427,12 @@
 
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
-       let 
-         (* FIXME: better exception handling *)  
-         fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^
-           Syntax.string_of_term ctxt rel ^ " :: " ^
-           Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^
-           Syntax.string_of_term ctxt rel' ^ " :: " ^
-           Syntax.string_of_typ ctxt (fastype_of rel') ^ "]")
+       let
          val rel_ty = fastype_of rel
          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') 
-       in 
-         if rel' aconv rel then rtrm else raise (exc rel rel')
-       end  
+       in
+         if rel' aconv rel then rtrm else relation_error ctxt rel rel'
+       end
 
   | (_, Const _) =>
        let