# HG changeset patch
# User webertj
# Date 1157027808 -7200
# Node ID 7e616709bca2b58a4e842cd4166bdead71e29968
# Parent  b222d9939e00d536276cd00e0403b293abc2d880
String.concatWith (not available in PolyML) replaced by space_implode

diff -r b222d9939e00 -r 7e616709bca2 src/HOL/Tools/res_atp.ML
--- 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];