diff -r 871fce48087f -r a0ddf16f05f5 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 15:33:06 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 15:36:49 2009 +0100
@@ -737,62 +737,24 @@
         else mk_repabs lthy (rty, qty) result
       end
   | _ =>
-      (**************************************************)
-      (*  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*)  
+        case (rhead, qhead) of
+          (Const _, Const _) =>
              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'
+        | (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 _, _ ) =>
+        | (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
-        val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
-      in
-        if rty = qty
-        then
-          case (rhead, qhead) of
-            (Free (_, T), Free (_, T')) =>
-              if T = T' then list_comb (rhead, rargs')
-              else list_comb (mk_repabs lthy (T, T') rhead, rargs')
-          | _ => list_comb (rhead, rargs')
-        else
-          case (rhead, qhead, length rargs') of
-            (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
-          | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead
-          | (Const _, Const _, _) =>  mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 
-          | (Free (x, T), Free (x', T'), _) => 
-               mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
-          | (Abs _, Abs _, _ ) =>
-               mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 
-          | _ => raise (LIFT_MATCH "injection")
-      end
-      *)
 end
 *}
 
@@ -1109,15 +1071,15 @@
  These rewrites can be done independently and in any order.
 
  - LAMBDA_PRS:
-     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x)))       \<equiv>   ?f
+     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))        ---->   f
  - Rewriting with definitions from the argument defs
-     (Abs) OldConst (Rep Args)                       \<equiv>   NewConst Args
+     (Abs) OldConst (Rep Args)                       ---->   NewConst Args
  - QUOTIENT_REL_REP:
-     Rel (Rep x) (Rep y)                             \<equiv>   x = y
+     Rel (Rep x) (Rep y)                             ---->   x = y
  - FORALL_PRS (and the same for exists: EXISTS_PRS)
-     \<forall>x\<in>Respects R. (abs ---> id) ?f                 \<equiv>   \<forall>x. ?f
+     \<forall>x\<in>Respects R. (abs ---> id) f                  ---->   \<forall>x. f
  - applic_prs
-     Abs1 ((Abs2 --> Rep1) f (Rep2 args))            \<equiv>   f args
+     Abs1 ((Abs2 --> Rep1) f (Rep2 args))            ---->   f args
 
  The first one is implemented as a conversion (fast).
  The second and third one are a simp_tac (fast).