--- a/IntEx.thy	Sat Nov 21 23:23:01 2009 +0100
+++ b/IntEx.thy	Sun Nov 22 00:01:06 2009 +0100
@@ -119,10 +119,6 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
-
-
-ML {* print_qconstinfo @{context} *}
-
 ML {* print_qconstinfo @{context} *}
 
 lemma plus_sym_pre:
@@ -165,18 +161,26 @@
 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
 done
 
+(* rep-abs injection *)
+
 ML {*
+(* FIXME: is this the right get_fun function for rep-abs injection *)
 fun mk_repabs lthy (T, T') trm = 
   Quotient_Def.get_fun repF lthy (T, T') 
   $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
 *}
 
 ML {*
+(* replaces a term for the bound variable, *)
+(* possible capture                        *)
 fun replace_bnd0 (trm, Abs (x, T, t)) =
   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 inj_REPABS lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm
@@ -184,34 +188,34 @@
 in
   case (rtrm, qtrm) of
     (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 yvar = Free (y, T)
-      val res = lambda yvar (inj_REPABS lthy (s, s'))
-    in
-      if T = T'
-      then res
-      else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
-    end
-  (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) 
+      let
+        val (y, s) = Term.dest_abs (x, T, t)
+        val (y', 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'
+        then 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 "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'))
-  | (rtrm as _ $ _, qtrm as _ $ _) => 
-    let
-      val (rhead, rargs) = Term.strip_comb rtrm
-      val (qhead, qargs) = Term.strip_comb qtrm
-      val rhead' = inj_REPABS lthy (rhead, qhead)
-      val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
-      val res = list_comb (rhead', rargs')
-    in
-      if rty = qty
-      then res
-      else mk_repabs lthy (rty, qty) res
-    end
-  (* FIXME: cases for frees and vars *)
+       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (_ $ _, _ $ _) => 
+      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')
+      in
+        if rty = qty
+        then result
+        else mk_repabs lthy (rty, qty) res
+      end
+  (* FIXME: cases for frees and vars? *)
   | _ => rtrm
 end
 *}
@@ -278,8 +282,8 @@
 ML {* cprem_of *}
 
 ML {* 
-(mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
-  |> Syntax.check_term @{context})
+mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
+  |> Syntax.check_term @{context}
 *}
 
 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
@@ -295,12 +299,6 @@
 *}
 
 
-
-
-
-
-
-
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
 done