# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277099188 -3600
# Node ID 7412424213eccbc04b810880b9e0143b990f4434
# Parent  08bbde090a17b07bfe9a05ef564fc9ff88574477
merged

diff -r 08bbde090a17 -r 7412424213ec Attic/Quot/quotient_term.ML
--- 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'