diff -r cfdd09041638 -r da12763acd6b src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Oct 12 19:53:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Oct 12 21:52:44 2014 +0200
@@ -730,7 +730,7 @@
     fun in_group group = member (op =) group o hd
     fun group_of skoX = find_first (fn group => in_group group skoX) groups
 
-    fun new_steps skoXss_steps group =
+    fun new_steps (skoXss_steps : (string list * (term, 'a) atp_step) list) group =
       let
         val name = step_name_of_group group
         val name0 = name |>> prefix "0"