src/HOL/Tools/res_atp.ML
changeset 20446 7e616709bca2
parent 20444 6c5e38a73db0
child 20457 85414caac94a
     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