diff -r dee1fd1cc631 -r 7f2b3b6f6ad1 src/HOL/Tools/SMT/smtlib_interface.ML
--- 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"