--- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 17 16:53:39 2014 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 17 17:32:27 2014 +0200
@@ -133,15 +133,18 @@
fun assert_name_of_index i = assert_prefix ^ string_of_int i
fun assert_index_of_name s = the_default ~1 (Int.fromString (unprefix assert_prefix s))
-fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
+fun serialize smt_options comments {logic, sorts, lfp_dtyps, gfp_dtyps, funcs} ts =
Buffer.empty
|> fold (Buffer.add o enclose "; " "\n") comments
|> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
|> Buffer.add logic
|> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
- |> (if null dtyps then I
+ |> (if null lfp_dtyps then I
else Buffer.add (enclose "(declare-datatypes () (" "))\n"
- (space_implode "\n " (maps (map sdatatype) dtyps))))
+ (space_implode "\n " (maps (map sdatatype) lfp_dtyps))))
+ |> (if null gfp_dtyps then I
+ else Buffer.add (enclose "(declare-codatatypes () (" "))\n"
+ (space_implode "\n " (maps (map sdatatype) gfp_dtyps))))
|> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
(sort (fast_string_ord o pairself fst) funcs)
|> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"