src/HOL/Tools/SMT/z3_proof_parser.ML

--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 11:28:10 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 11:34:54 2011 +0200
@@ -148,13 +148,11 @@
 end
 
 local
-  fun equal_var cv (_, cu) = (cv aconvc cu)
-
   fun prep (ct, vars) (maxidx, all_vars) =
     let
       val maxidx' = maxidx + maxidx_of ct + 1
 
-      fun part (v as (i, cv)) =
+      fun part (i, cv) =
         (case AList.lookup (op =) all_vars i of
           SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
         | NONE =>