--- 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