diff -r a98b136fc88a -r c10a46fa0de9 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 11:38:58 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 11:59:16 2009 +0100
@@ -602,7 +602,12 @@
        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
 
   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
-       Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+      let
+        val rty = fastype_of rtrm
+        val qty = fastype_of qtrm
+      in
+        mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
+      end
 
   | (Abs (x, T, t), Abs (x', T', t')) =>
       let