diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -11,11 +11,11 @@
 
   (*built-in types*)
   val add_builtin_typ: SMT_Util.class ->
-    typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+    typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
     Context.generic
   val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
     Context.generic
-  val dest_builtin_typ: Proof.context -> typ -> string option
+  val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
   val is_builtin_typ_ext: Proof.context -> typ -> bool
 
   (*built-in numbers*)
@@ -93,7 +93,8 @@
 structure Builtins = Generic_Data
 (
   type T =
-    (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+    (Proof.context -> typ -> bool,
+     (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
     (term list bfun, bfunr option bfun) btab
   val empty = ([], Symtab.empty)
   val extend = I