diff -r 047bb4a9466c -r 11b48e7a4e7e src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 14:27:43 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 14:58:30 2013 +0200
@@ -78,7 +78,7 @@
   in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
 
 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
-  | term_name' t = ""
+  | term_name' _ = ""
 
 fun lambda' v = Term.lambda_name (term_name' v, v)