1.1 --- a/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 20:40:42 2010 +0200
     1.2 +++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 20:40:42 2010 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4  
     1.5  (* serialization *)
     1.6  
     1.7 -fun wr s stream = (TextIO.output (stream, s); stream)
     1.8 +val wr = Buffer.add
     1.9  fun wr_line f = f #> wr "\n"
    1.10  
    1.11  fun sep f = wr " " #> f
    1.12 @@ -118,11 +118,10 @@
    1.13            | wr_pat (T.SNoPat ts) = wrp "nopat" ts
    1.14        in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
    1.15  
    1.16 -fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream =
    1.17 -  let
    1.18 -    fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
    1.19 +fun serialize attributes comments ({typs, funs, preds} : T.sign) ts =
    1.20 +  let fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
    1.21    in
    1.22 -    stream
    1.23 +    Buffer.empty
    1.24      |> wr_line (wr "(benchmark Isabelle")
    1.25      |> wr_line (wr ":status unknown")
    1.26      |> fold (wr_line o wr) attributes
    1.27 @@ -140,7 +139,7 @@
    1.28      |> wr_line (wr ":formula true")
    1.29      |> wr_line (wr ")")
    1.30      |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
    1.31 -    |> K ()
    1.32 +    |> Buffer.content
    1.33    end
    1.34  
    1.35