--- a/IntEx.thy	Mon Nov 23 13:24:12 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 13:46:14 2009 +0100
@@ -177,10 +177,13 @@
   Abs (x, T, subst_bound (trm, t))
 *}
 
+
 ML {*
 (* 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
@@ -206,26 +209,20 @@
              then mk_repabs lthy (rty, qty) res
              else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
       end
-    (* TODO: check what happens if head is a constant *)
-  | (_ $ _, _ $ _) => 
+  | _ =>
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
-        val rhead' = inj_REPABS lthy (rhead, qhead)
-        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
-        val result = list_comb (rhead', rargs')
+        (* TODO:  val rhead' = inj_REPABS lthy (rhead, qhead) *)
+        val rhead' = rhead;
+        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs);
+        val result = list_comb (rhead', rargs');
       in
-        if rty = qty
-        then result
-        else mk_repabs lthy (rty, qty) 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
-  (* TODO: maybe leave result without mk_repabs when head is a constant *)
-  (* TODO: that we do not know how to lift *)
-  | (Const (s, T), Const (s', T')) =>
-       if T = T'
-       then rtrm
-       else mk_repabs lthy (T, T') rtrm
-  | _ => rtrm
 end
 *}