# HG changeset patch
# User wenzelm
# Date 1267222047 -3600
# Node ID 34d8e0a9bfa7409629d04ee41658b57ee09a2eb0
# Parent  efad0e36473825573dbde36f05a234a36cb5ddb5
tuned;

diff -r efad0e364738 -r 34d8e0a9bfa7 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 23:05:47 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 23:07:27 2010 +0100
@@ -52,7 +52,7 @@
 fun mk_syntax name i =
   let
     val syn = Syntax.escape name
-    val args = concat (separate ",/ " (replicate i "_"))
+    val args = space_implode ",/ " (replicate i "_")
   in
     if i = 0 then Mixfix (syn, [], 1000)
     else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)