tuned;
authorwenzelm
Fri Feb 26 23:07:27 2010 +0100 (2010-02-26)
changeset 3539134d8e0a9bfa7
parent 35390 efad0e364738
child 35392 5da5ac6c6b77
tuned;
src/HOL/Boogie/Tools/boogie_loader.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 23:05:47 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Feb 26 23:07:27 2010 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  fun mk_syntax name i =
     1.5    let
     1.6      val syn = Syntax.escape name
     1.7 -    val args = concat (separate ",/ " (replicate i "_"))
     1.8 +    val args = space_implode ",/ " (replicate i "_")
     1.9    in
    1.10      if i = 0 then Mixfix (syn, [], 1000)
    1.11      else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000)