src/HOL/SMT/Tools/smtlib_interface.ML

         fun wrp s ts = wr1 (":" ^ s ^ "{") #> ins "," wre ts #> wr1 "}"
         fun wr_pat (T.SPat ts) = wrp "pat" ts
           | wr_pat (T.SNoPat ts) = wrp "nopat" ts
       in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
 
-fun serialize attributes (T.Sign {typs, funs, preds}) ts stream =
+fun serialize attributes ({typs, funs, preds} : T.sign) ts stream =
   let
     fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
   in
     stream
     |> wr_line (wr "(benchmark Isabelle")

   end
 
 
 (* SMT solver interface using the SMT-LIB input format *)
 
-val basic_builtins = T.Builtins {
+val basic_builtins = {
   builtin_typ = builtin_typ,
   builtin_num = builtin_num,
   builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
 
 val default_attributes = [":logic AUFLIRA", ":status unknown"]
 
-fun gen_interface builtins attributes = SMT_Solver.Interface {
+fun gen_interface builtins attributes = {
   normalize = [
     SMT_Normalize.RewriteTrivialLets,
     SMT_Normalize.RewriteNegativeNumerals,
     SMT_Normalize.RewriteNaturalNumbers,
     SMT_Normalize.AddAbsMinMaxRules,
     SMT_Normalize.AddPairRules,
     SMT_Normalize.AddFunUpdRules ],
-  translate = T.Config {
+  translate = {
     strict = true,
-    prefixes = T.Prefixes {
+    prefixes = {
       var_prefix = "x",
       typ_prefix = "T",
       fun_prefix = "uf_",
       pred_prefix = "up_" },
-    markers = T.Markers {
+    markers = {
       term_marker = term_marker,
       formula_marker = formula_marker },
     builtins = builtins,
     serialize = serialize attributes }}