String.concatWith (not available in PolyML) replaced by space_implode

--- a/src/HOL/Tools/res_atp.ML	Thu Aug 31 10:20:22 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Aug 31 14:36:48 2006 +0200
@@ -480,7 +480,7 @@
   case rev (String.fields (fn c => c = #"_") s) of
       last::rest => 
           if all_numeric last 
-          then [s, String.concatWith "_" (rev rest)]
+          then [s, space_implode "_" (rev rest)]
           else [s]
     | [] => [s];