# HG changeset patch
# User blanchet
# Date 1387269758 -3600
# Node ID bddb91fb8e374a78261f994d1203629e8f39928c
# Parent  79f66cd15d573ea1c1683056eea27d222bdb57ee
made SML/NJ happier

diff -r 79f66cd15d57 -r bddb91fb8e37 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 23:36:54 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Dec 17 09:42:38 2013 +0100
@@ -570,7 +570,7 @@
         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