--- a/QuotMain.thy	Sat Dec 05 22:07:46 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 22:16:17 2009 +0100
@@ -703,24 +703,12 @@
 *}
 
 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 *)
+(* bound variables need to be treated properly,    *)
+(* as the type of subterms need to be calculated   *)
+(* in the abstraction case                         *)
 
 fun inj_repabs_trm lthy (rtrm, qtrm) =
-let
-  val rty = fastype_of rtrm
-  val qty = fastype_of qtrm
-in
-  case (rtrm, qtrm) of
+ 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'))
 
@@ -732,6 +720,8 @@
 
   | (Abs (x, T, t), Abs (x', T', t')) =>
       let
+        val rty = fastype_of rtrm
+        val qty = fastype_of qtrm
         val (y, s) = Term.dest_abs (x, T, t)
         val (_, s') = Term.dest_abs (x', T', t')
         val yvar = Free (y, T)
@@ -745,12 +735,12 @@
   | (t $ s, t' $ s') =>  
        (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
 
-  | (Free (x, T), Free (x', T')) => 
+  | (Free (_, T), Free (_, T')) => 
         if T = T' 
         then rtrm 
         else mk_repabs lthy (T, T') rtrm
 
-  | (Const (s, T), Const (s', T')) =>
+  | (Const (_, T), Const (_, T')) =>
         if T = T'                    
         then rtrm
         else mk_repabs lthy (T, T') rtrm
@@ -758,7 +748,6 @@
   | (_, Const (@{const_name "op ="}, _)) => rtrm
   
   | _ => raise (LIFT_MATCH "injection")
-end
 *}
 
 section {* RepAbs Injection Tactic *}