tuned;

--- 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)