--- a/IntEx.thy	Sat Dec 05 00:06:27 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 13:49:35 2009 +0100
@@ -149,6 +149,36 @@
 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
+lemma test1: "my_plus a b = my_plus a b"
+apply(rule refl)
+done
+
+lemma "PLUS a b = PLUS a b"
+apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+(* does not work yet *)
+oops
+
+lemma test2: "my_plus a = my_plus a"
+apply(rule refl)
+done
+
+lemma "PLUS a = PLUS a"
+apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
+(* does not work yet *)
+oops
+
+lemma test3: "my_plus = my_plus"
+apply(rule refl)
+done
+
+lemma "PLUS = PLUS"
+apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
+apply(rule ho_plus_rsp)
+(* does not work yet *)
+oops
+
 
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})

--- a/QuotMain.thy	Sat Dec 05 00:06:27 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 13:49:35 2009 +0100
@@ -470,8 +470,6 @@
        then rtrm 
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
-  
-
   | (rt, qt) =>
        raise (LIFT_MATCH "regularize (default)")
 *}
@@ -702,6 +700,15 @@
 *}
 
 ML {*
+fun strip_combn n u =
+    let fun stripc 0 x = x
+        |   stripc n (f $ t, ts) = stripc (n - 1) (f, t::ts)
+        |   stripc _ x =  x
+    in  stripc n (u, [])  end
+*}
+
+
+ML {*
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
 
@@ -713,10 +720,13 @@
   case (rtrm, qtrm) of
     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
        Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+
   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
-  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
+
+  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
        Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+
   | (Abs (x, T, t), Abs (x', T', t')) =>
       let
         val (y, s) = Term.dest_abs (x, T, t)
@@ -730,8 +740,8 @@
       end
   | _ =>
       let
-        val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
+        val (rhead, rargs) = strip_combn (length qargs) rtrm
         val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
       in
         case (rhead, qhead) of
@@ -745,7 +755,12 @@
              else list_comb (mk_repabs lthy (T, T') rhead, rargs')
         | (Abs _, Abs _) =>
              list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') 
-        | _ => raise (LIFT_MATCH "injection")
+ 
+        (* FIXME: when there is an (op =), then lhs might have been a term *) 
+        | (_, Const (@{const_name "op ="}, T)) =>
+             list_comb (rhead, rargs')
+        | _ => raise (LIFT_MATCH ("injection: rhead: " ^ (Syntax.string_of_term lthy rhead) 
+                                          ^ " qhead: " ^ (Syntax.string_of_term lthy qhead)))
       end
 end
 *}
@@ -1220,9 +1235,11 @@
   val reg_goal = 
         Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
         handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+  val _ = tracing "Regularization done."
   val inj_goal = 
         Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
         handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+  val _ = tracing "RepAbs Injection done."
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),