# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259048104 -3600
# Node ID abc6bfd0576e31863d552c88238b4ee79d84ce53
# Parent  2eb6d527dfe4b75b5f29fe982b39030303d0a15a
More fixes for inj_REPABS

diff -r 2eb6d527dfe4 -r abc6bfd0576e QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 01:36:50 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 08:35:04 2009 +0100
@@ -1419,11 +1419,16 @@
         val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
       in
         if rty = qty
-        then list_comb (rhead, rargs')
+        then
+          case (rhead, qhead) of
+            (Free (_, T), Free (_, T')) =>
+              if T = T' then list_comb (rhead, rargs')
+              else list_comb (mk_repabs lthy (T, T') rhead, rargs')
+          | _ => list_comb (rhead, rargs')
         else
           case (rhead, qhead, length rargs') of
             (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
-          | (Free  _, Free  _, 0) =>  mk_repabs lthy (rty, qty) rhead
+          | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead
           | (Const _, Const _, _) =>  mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 
           | (Free (x, T), Free (x', T'), _) => 
                mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))