src/HOL/Tools/ATP/atp_proof_reconstruct.ML

 
     fun step_name_of_group skoXs = (implode skoXs, [])
     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"
         val t =
           (case map (snd #> #3) skoXss_steps of