diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index bdcf1a26b..f34ce0ca7 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -374,6 +374,10 @@ struct
   let sort_lton ( a : sort list ) =
     let f ( e : sort ) = match e with Sort(a) -> (AST.ptr_of_ast a) in 
     Array.of_list (List.map f a)
+
+  let sort_option_lton ( a : sort option list ) =
+    let f ( e : sort option ) = match e with None -> null | Some(Sort(a)) -> (AST.ptr_of_ast a) in 
+    Array.of_list (List.map f a)
     
   let equal : sort -> sort -> bool = fun a b ->
     (a == b) ||
@@ -1257,7 +1261,7 @@ struct
     
     let _sizes = Hashtbl.create 0
 
-    let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort list ) ( sort_refs : int list ) =
+    let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
       let n = (List.length field_names) in
       if n != (List.length sorts) then
 	raise (Z3native.Exception "Number of field names does not match number of sorts")
@@ -1269,7 +1273,7 @@ struct
 		       (Symbol.gno recognizer) 
 		       n
 		       (Symbol.symbol_lton field_names)
-		       (sort_lton sorts)
+		       (sort_option_lton sorts)
 		       (Array.of_list sort_refs)) in
 	  let no : constructor = { m_ctx = ctx ;
 				   m_n_obj = null ;
@@ -1316,11 +1320,11 @@ struct
       res       
   end
     
-  let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort list ) ( sort_refs : int list ) =
+  let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
     Constructor.create ctx name recognizer field_names sorts sort_refs
 
 
-  let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort list ) ( sort_refs : int list ) =
+  let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
     mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs
 
   let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor list ) =
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 4347c7431..1342bb4bc 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -1053,12 +1053,12 @@ sig
   (** Create a datatype constructor.
      if the corresponding sort reference is 0, then the value in sort_refs should be an index 
      referring to one of the recursive datatypes that is declared. *)
-  val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort list -> int list -> Constructor.constructor
+  val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
 
   (** Create a datatype constructor.
      if the corresponding sort reference is 0, then the value in sort_refs should be an index 
      referring to one of the recursive datatypes that is declared. *)
-  val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort list -> int list -> Constructor.constructor
+  val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor
 
   (** Create a new datatype sort. *)
   val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort