String.concatWith (not available in PolyML) replaced by space_implode
authorwebertj
Thu Aug 31 14:36:48 2006 +0200 (2006-08-31 ago)
changeset 204467e616709bca2
parent 20445 b222d9939e00
child 20447 5b75f1c4d7d6
String.concatWith (not available in PolyML) replaced by space_implode
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Aug 31 10:20:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Aug 31 14:36:48 2006 +0200
     1.3 @@ -480,7 +480,7 @@
     1.4    case rev (String.fields (fn c => c = #"_") s) of
     1.5        last::rest => 
     1.6            if all_numeric last 
     1.7 -          then [s, String.concatWith "_" (rev rest)]
     1.8 +          then [s, space_implode "_" (rev rest)]
     1.9            else [s]
    1.10      | [] => [s];
    1.11