diff -r 7851e2a74f85 -r 5a7024be9083 IntEx.thy
--- a/IntEx.thy	Mon Nov 23 10:26:59 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 13:24:12 2009 +0100
@@ -187,22 +187,26 @@
   val qty = fastype_of qtrm
 in
   case (rtrm, qtrm) of
-    (Abs (x, T, t), Abs (x', T', t')) =>
+    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
+       Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Abs (x, T, t), Abs (x', T', t')) =>
       let
         val (y, s) = Term.dest_abs (x, T, t)
-        val (y', s') = Term.dest_abs (x', T', t')
+        val (_, s') = Term.dest_abs (x', T', t')
         val yvar = Free (y, T)
         val res = lambda yvar (inj_REPABS lthy (s, s'))
       in
-        if T = T'
+        if rty = qty
         then res
-        else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), 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
-  (* FIXME: Does one have to look at the abstraction or have to go under the lambda? *) 
-  | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
-  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+    (* TODO: check what happens if head is a constant *)
   | (_ $ _, _ $ _) => 
       let
         val (rhead, rargs) = strip_comb rtrm
@@ -213,9 +217,14 @@
       in
         if rty = qty
         then result
-        else mk_repabs lthy (rty, qty) res
+        else mk_repabs lthy (rty, qty) result
       end
-  (* FIXME: cases for frees and vars? *)
+  (* 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
 *}
@@ -286,6 +295,10 @@
   |> Syntax.check_term @{context}
 *}
 
+
+ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
+ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
+
 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 (* does not work *)