src/HOL/Tools/ATP/atp_proof_reconstruct.ML

 
         fun step_name_of_group skos = (implode skos, [])
         fun in_group group = member (op =) group o hd
         fun group_of sko = the (find_first (fn group => in_group group sko) groups)
 
-        fun new_step group skoss_steps =
+        fun new_step group (skoss_steps : ('a * (term, 'b) atp_step) list) =
           let
             val t =
               skoss_steps
               |> map (snd #> #3 #> HOLogic.dest_Trueprop)
               |> Library.foldr1 s_conj