--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Dec 31 00:11:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Jan 03 16:22:08 2011 +0100
@@ -130,10 +130,10 @@
fun sdatatypes decls =
let
- fun con (n, []) = add n
+ fun con (n, []) = sep (add n)
| con (n, sels) = par (add n #>
- fold (fn (n, s) => sep (par (add n #> sep (add s)))) sels)
- fun dtyp (n, decl) = add n #> fold (sep o con) decl
+ fold (fn (n, s) => par (add n #> sep (add s))) sels)
+ fun dtyp (n, decl) = add n #> fold con decl
in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
fun serialize comments {header, sorts, dtyps, funcs} ts =