--- a/QuotMain.thy	Mon Nov 23 15:08:09 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 15:08:25 2009 +0100
@@ -1385,6 +1385,10 @@
 (* possible capture                        *)
 fun replace_bnd0 (trm, Abs (x, T, t)) =
   Abs (x, T, subst_bound (trm, t))
+
+(* FIXME: this should be a proper test with the qcinfo *)
+fun is_lifted_const h gh = 
+  is_Const h andalso is_Const gh andalso not (h = gh)
 *}
 
 
@@ -1392,8 +1396,6 @@
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
 
-fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
-
 fun inj_REPABS lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm
@@ -1413,11 +1415,11 @@
         val yvar = Free (y, T)
         val res = lambda yvar (inj_REPABS lthy (s, s'))
       in
-        if rty = qty
-        then res
-        else if T = T'
-             then mk_repabs lthy (rty, qty) res
-             else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
+        if rty = qty then 
+          res
+        else if T = T' then 
+          mk_repabs lthy (rty, qty) res
+        else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
       end
   | _ =>
       let
@@ -1428,10 +1430,15 @@
         val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs);
         val result = list_comb (rhead', rargs');
       in
-        if rty = qty then result else
-        if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else
-        if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else
-        if rargs' = [] then rhead' else result
+        if rty = qty then 
+          result 
+        else if (is_lifted_const rhead qhead) then 
+          mk_repabs lthy (rty, qty) result 
+        else if ((Term.is_Free rhead) andalso (length rargs' > 0)) then 
+          mk_repabs lthy (rty, qty) result 
+        else if rargs' = [] then 
+          rhead' 
+        else result
       end
 end
 *}