diff -r 129caba33c03 -r fb7fe6aca6f0 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Mon Jan 11 00:31:29 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Jan 11 01:03:34 2010 +0100
@@ -199,9 +199,7 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             (*if tys' = [] orelse tys' = tys 
-             then absrep_const flag ctxt s'
-             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
+             mk_fun_compose flag (absrep_const flag ctxt s', result)
            end
     | (TFree x, TFree x') =>
         if x = x'
@@ -300,9 +298,7 @@
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
-           (*if tys' = [] orelse tys' = tys 
-           then eqv_rel'
-           else*) mk_rel_compose (result, eqv_rel')
+           mk_rel_compose (result, eqv_rel')
          end
       | _ => HOLogic.eq_const rty
 
@@ -402,6 +398,7 @@
   | (* 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[" ^