--- a/QuotMain.thy	Sun Nov 29 19:48:55 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 23:59:37 2009 +0100
@@ -343,64 +343,6 @@
   end
 *}
 
-section {* Infrastructure for special quotient identity *}
-
-definition
-  "qid TYPE('a) TYPE('b) x \<equiv> x"
-
-ML {*
-fun get_typ1 (Type ("itself", [T])) = T 
-fun get_typ2 (Const ("TYPE", T)) = get_typ1 T
-fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =
-  (get_typ2 ty1, get_typ2 ty2)
-
-fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true
-  | is_qid _ = false
-
-
-fun mk_itself ty = Type ("itself", [ty])
-fun mk_TYPE ty = Const ("TYPE", mk_itself ty)
-fun mk_qid (rty, qty, trm) = 
-  Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) 
-    $ mk_TYPE rty $ mk_TYPE qty $ trm
-*}
-
-ML {*
-fun insertion_aux rtrm qtrm =
-  case (rtrm, qtrm) of
-    (Abs (x, ty, t), Abs (x', ty', t')) =>
-       let
-         val (y, s) = Term.dest_abs (x, ty, t)
-         val (_, s') = Term.dest_abs (x', ty', t')
-         val yvar = Free (y, ty)
-         val result = Term.lambda_name (y, yvar) (insertion_aux s s')
-       in     
-         if ty = ty'
-         then result
-         else mk_qid (ty, ty', result)
-       end
-  | (t1 $ t2, t1' $ t2') =>
-       let 
-         val rty = fastype_of rtrm
-         val qty = fastype_of qtrm 
-         val subtrm1 = insertion_aux t1 t1' 
-         val subtrm2 = insertion_aux t2 t2'
-       in
-         if rty = qty
-         then subtrm1 $ subtrm2
-         else mk_qid (rty, qty, subtrm1 $ subtrm2)
-       end
-  | (Free (_, ty), Free (_, ty')) =>
-       if ty = ty'
-       then rtrm 
-       else mk_qid (ty, ty', rtrm)
-  | (Const (s, ty), Const (s', ty')) =>
-       if s = s' andalso ty = ty'
-       then rtrm
-       else mk_qid (ty, ty', rtrm) 
-  | (_, _) => raise (LIFT_MATCH "insertion")
-*}
-
 section {* Regularization *} 
 
 (*
@@ -794,10 +736,38 @@
         else mk_repabs lthy (rty, qty) result
       end
   | _ =>
-      (* FIXME / TODO: this is a case that needs to be looked at          *)
-      (* - variables get a rep-abs insde and outside an application       *)
-      (* - constants only get a rep-abs on the outside of the application *)
-      (* - applications get a rep-abs insde and outside an application    *)
+      (**************************************************)
+      (*  new
+      let
+        val (rhead, rargs) = strip_comb rtrm
+        val (qhead, qargs) = strip_comb qtrm
+        val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
+      in
+        case (rhead, qhead, length rargs') of
+          (Const (_, T), Const (_, T'), 0) => 
+             if T = T'
+             then rhead 
+             else mk_repabs lthy (T, T') rhead
+        | (Free (_, T), Free (_, T'), 0) => 
+             if T = T'
+             then rhead 
+             else mk_repabs lthy (T, T') rhead
+        | (Const (_, T), Const (_, T'), _) => (* FIXME/TODO: check this case exactly*)  
+             if rty = qty                   
+             then list_comb (rhead, rargs') 
+             else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 
+        | (Free (x, T), Free (x', T'), _) => 
+             if T = T'
+             then list_comb (rhead, rargs')
+             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")
+      end
+      *)
+
+      (*************************************************)
+      (* old *)
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
@@ -821,6 +791,7 @@
                mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 
           | _ => raise (LIFT_MATCH "injection")
       end
+      (**)
 end
 *}