src/HOL/SMT/Tools/smtlib_interface.ML

   (@{term "op <= :: real => _"}, "<=") ]
 
 
 (* serialization *)
 
-fun wr s stream = (TextIO.output (stream, s); stream)
+val wr = Buffer.add
 fun wr_line f = f #> wr "\n"
 
 fun sep f = wr " " #> f
 fun par f = sep (wr "(" #> f #> wr ")")
 

         fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}"
         fun wr_pat (T.SPat ts) = wrp "pat" ts
           | wr_pat (T.SNoPat ts) = wrp "nopat" ts
       in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
 
-fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream =
-  let
-    fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
+fun serialize attributes comments ({typs, funs, preds} : T.sign) ts =
+  let fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
   in
-    stream
+    Buffer.empty
     |> wr_line (wr "(benchmark Isabelle")
     |> wr_line (wr ":status unknown")
     |> fold (wr_line o wr) attributes
     |> length typs > 0 ?
          wr_line (wr ":extrasorts" #> par (fold wr1 typs))

          wr_line (wr " )"))
     |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
     |> wr_line (wr ":formula true")
     |> wr_line (wr ")")
     |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
-    |> K ()
+    |> Buffer.content
   end
 
 
 (* SMT solver interface using the SMT-LIB input format *)