diff -r 565f9af86d67 -r 41a109a00c53 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 18 16:50:14 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 18 17:00:14 2013 +0100
@@ -220,15 +220,15 @@
 val skip_term =
   let
     fun skip _ accum [] = (accum, [])
-      | skip n accum (s :: ss) =
+      | skip n accum (ss as s :: ss') =
         if s = "," andalso n = 0 then
           (accum, ss)
         else if member (op =) [")", "]", ">", "}"] s then
-          if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss
+          if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss'
         else if member (op =) ["(", "[", "<", "{"] s then
-          skip (n + 1) (s :: accum) ss
+          skip (n + 1) (s :: accum) ss'
         else
-          skip n (s :: accum) ss
+          skip n (s :: accum) ss'
   in
     skip 0 [] #>> (rev #> implode)
   end