--- ./src/encoding_pred.ml.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./src/encoding_pred.ml	2012-07-31 15:35:10.506221997 -0600
@@ -266,11 +266,6 @@ let rec push d =
 	| Pnamed (s, p) ->
 	    Pnamed (s, translate_eq p) 
 	| p -> p in
-      let rec lifted  l p =
-	match l with [] -> p
-	| (_,a)::q -> 
-	    lifted q (Forall(false, Ident.create a, Ident.create a, ut, [], p))
-      in
       Queue.add (Dgoal
 		   (loc, is_lemma, expl, name,
 		    Env.empty_scheme
--- ./src/encoding_rec.ml.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./src/encoding_rec.ml	2012-07-31 15:35:10.506221997 -0600
@@ -397,11 +397,6 @@ let rec push d =
 	| Tconst (ConstUnit) as t -> plunge fv t PTunit
 	| Tconst (ConstFloat _) as t -> plunge fv t PTreal
 	| _ as t -> t in
-      let rec lifted  l p =
-	match l with [] -> p
-	| (_,a)::q -> 
-	    lifted q (Forall(false, Ident.create a, Ident.create a, ut, [], p))
-      in
       Queue.add (Dgoal 
 		   (loc, is_lemma, expl, name,
 		    Env.empty_scheme 
--- ./src/theoryreducer.ml.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./src/theoryreducer.ml	2012-07-31 15:35:10.507222001 -0600
@@ -191,11 +191,6 @@ struct
     (** symbols the result **)
     let symbolsSet  = ref StringSet.empty  in 
     let rec collect formula  = 
-      let rec collectIntoAList  l = match l with 
-	  [] -> () 
-	|  p :: r -> 
-	     collect p ;
-	     collectIntoAList r in 
       match formula with 
 	| Papp (id, [a; b], _) when is_eq id || is_neq id || id == t_zwf_zero->
 	    symbolsSet  := StringSet.union (functionalSymbolsCollect a) 
--- ./src/vcg.ml.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./src/vcg.ml	2012-07-31 15:35:10.507222001 -0600
@@ -615,13 +615,6 @@ let occur_as_var id = function
   | Spred _ -> false
 
 let clean_sequent hyps concl =
-  (* if a variable appears twice, we remove the first and its dependencies *)
-  let rec filter_up_to x = function
-    | [] -> []
-    | Svar (y, _) :: _ as hl when x = y -> hl
-    | Spred (_, p) :: hl when occur_predicate x p -> filter_up_to x hl
-    | h :: hl -> h :: filter_up_to x hl
-  in
   (* we remove variables not occuring at all in hypotheses or conclusion *)
   let rec clean = function
     | [] ->
--- ./src/theory_filtering.ml.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./src/theory_filtering.ml	2012-07-31 15:35:10.507222001 -0600
@@ -180,11 +180,6 @@ let symbols  f  =
   (** symbols the result **)
   let symbolsSet  = ref Int_set.empty  in 
   let rec collect formula  = 
-    let rec collectIntoAList  l = match l with 
-	[] -> () 
-      |  p :: r -> 
-	   collect p ;
-	   collectIntoAList r in 
     match formula with 
       | Papp (id, [a; b], _) when is_eq id || is_neq id || id == t_zwf_zero->
 	  symbolsSet  := Int_set.union (functional_symbols a) 
--- ./jc/jc_iterators.ml.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./jc/jc_iterators.ml	2012-07-31 15:35:52.481285428 -0600
@@ -1057,13 +1057,6 @@ let replace_sub_expr e el =
     | None -> None,el 
     | Some _ -> let e1,r = pop el in Some e1,r
   in
-  let rec popn n el = 
-    if n > 0 then 
-      let e,r = pop el in
-      let el1,el2 = popn (n-1) r in
-      e :: el1, el2
-    else [],el
-  in
   let enode = match e#node with
     | JCEconst _ | JCEvar _ | JCEassert _ | JCEreturn_void as enode -> enode
     | JCEcontract(req,dec,vi_result,behs,_e) ->