src/HOL/Tools/SMT/smtlib_interface.ML

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 17 20:57:11 2025 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 19 13:11:51 2025 +0200
@@ -13,6 +13,14 @@
   val realsmlibC: SMT_Util.class
   val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
+
+  type dtype_decls = (string * (string * (string * string) list) list) list
+  type func_decl = string * (string list * string)
+  val serialize: (BNF_Util.fp_kind * dtype_decls -> Buffer.T -> Buffer.T) -> (string * string) list -> string list ->
+    {dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
+     funcs: func_decl list, logic: string, sorts: string list} ->
+    (SMT_Util.role * SMT_Translate.sterm) list -> string
+
   val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
   val assert_name_of_role_and_index: SMT_Util.role -> int -> string
   val role_and_index_of_assert_name: string -> SMT_Util.role * int
@@ -157,11 +165,16 @@
 fun role_and_index_of_assert_name s =
   apsnd (the_default ~1 o Int.fromString) (unprefix_axiom s)
 
-fun sdtyp (fp, dtyps) =
+type dtype_decls = (string * (string * (string * string) list) list) list
+
+fun sdtyp (fp, dtyps : dtype_decls) =
   Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
     (space_implode "\n  " (map sdatatype dtyps)))
 
-fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
+type func_decl = string * (string list * string)
+
+fun serialize (sdtyp : BNF_Util.fp_kind * dtype_decls -> Buffer.T -> Buffer.T) smt_options comments
+      {logic, sorts, dtyps, funcs} ts =
   let
     val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
   in
@@ -187,7 +200,7 @@
   order = order,
   logic = choose_logic ctxt,
   fp_kinds = [],
-  serialize = serialize}
+  serialize = serialize sdtyp}
 
 val _ = Theory.setup (Context.theory_map
   (setup_builtins #>