diff -r 42b90994ac77 -r 89d772dae4d4 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 08 15:02:12 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 08 19:46:22 2010 +0100
@@ -187,8 +187,9 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             mk_fun_compose flag (absrep_const flag ctxt s', result)
-           end 
+             if tys' = [] orelse tys' = tys then absrep_const flag ctxt s'
+             else mk_fun_compose flag (absrep_const flag ctxt s', result)
+           end
     | (TFree x, TFree x') =>
         if x = x'
         then mk_identity rty
@@ -289,8 +290,9 @@
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
-           mk_rel_compose (result, eqv_rel')
-         end  
+           if tys' = [] orelse tys' = tys then eqv_rel'
+           else mk_rel_compose (result, eqv_rel')
+         end
       | _ => HOLogic.eq_const rty
 
 fun new_equiv_relation_chk ctxt (rty, qty) =
@@ -386,7 +388,7 @@
          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
        in
          if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
+         else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
@@ -394,7 +396,7 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
@@ -402,22 +404,26 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm
-         else equiv_relation ctxt (domain_type ty, domain_type ty') 
+         else new_equiv_relation ctxt (domain_type ty, domain_type ty') 
 
   | (* in this case we just check whether the given equivalence relation is correct *) 
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
-         val exc = LIFT_MATCH "regularise (relation mismatch)"
+         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') ^ "]")
          val rel_ty = fastype_of rel
-         val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') 
+         val rel' = new_equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') 
        in 
-         if rel' aconv rel then rtrm else raise exc
+         if rel' aconv rel then rtrm else raise (exc rel rel')
        end  
 
   | (_, Const _) =>