--- a/Attic/Quot/quotient_term.ML	Fri Jun 11 03:02:42 2010 +0200
+++ b/Attic/Quot/quotient_term.ML	Mon Jun 21 06:46:28 2010 +0100
@@ -224,9 +224,9 @@
              val map_fun = mk_mapfun ctxt vs rty_pat
              val result = list_comb (map_fun, args)
            in
-             if forall is_identity args
+             (*if forall is_identity args
              then absrep_const flag ctxt s'
-             else mk_fun_compose flag (absrep_const flag ctxt s', result)
+             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
            end
     | (TFree x, TFree x') =>
         if x = x'