src/HOL/Tools/SMT/smt_builtin.ML

 fun lookup_btab ctxt btab (n, T) =
   (case Symtab.lookup btab n of
     NONE => NONE
   | SOME ttab => lookup_ttab ctxt ttab T)
 
-
-(* built-in types *)
-
-(* FIXME just one data slot (record) per program unit *)
-structure Builtin_Types = Generic_Data
+type 'a bfun = Proof.context -> typ -> term list -> 'a
+
+type bfunr = string * int * term list * (term list -> term)
+
+structure Builtins = Generic_Data
 (
   type T =
-    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
-  val empty = []
+    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+    (term list bfun, bfunr option bfun) btab
+  val empty = ([], Symtab.empty)
   val extend = I
-  val merge = merge_ttab
+  fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
 )
 
+(* built-in types *)
+
 fun add_builtin_typ cs (T, f, g) =
-  Builtin_Types.map (insert_ttab cs T (Int (f, g)))
+  Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
 
 fun add_builtin_typ_ext (T, f) =
-  Builtin_Types.map (insert_ttab SMT_Utils.basicC T (Ext f))
+  Builtins.map (apfst (insert_ttab SMT_Utils.basicC T (Ext f)))
 
 fun lookup_builtin_typ ctxt =
-  lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
+  lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
 
 fun dest_builtin_typ ctxt T =
   (case lookup_builtin_typ ctxt T of
     SOME (_, Int (f, _)) => f T
   | _ => NONE) 

   | SOME (T, _) => is_builtin_typ_ext ctxt T)
 
 
 (* built-in functions *)
 
-type 'a bfun = Proof.context -> typ -> term list -> 'a
-
-type bfunr = string * int * term list * (term list -> term)
-
-(* FIXME just one data slot (record) per program unit *)
-structure Builtin_Funcs = Generic_Data
-(
-  type T = (term list bfun, bfunr option bfun) btab
-  val empty = Symtab.empty
-  val extend = I
-  val merge = merge_btab
-)
-
 fun add_builtin_fun cs ((n, T), f) =
-  Builtin_Funcs.map (insert_btab cs n T (Int f))
+  Builtins.map (apsnd (insert_btab cs n T (Int f)))
 
 fun add_builtin_fun' cs (t, n) =
   let
     val c as (m, T) = Term.dest_Const t
     fun app U ts = Term.list_comb (Const (m, U), ts)
     fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
   in add_builtin_fun cs (c, bfun) end
 
 fun add_builtin_fun_ext ((n, T), f) =
-  Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f))
+  Builtins.map (apsnd (insert_btab SMT_Utils.basicC n T (Ext f)))
 
 fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
 
 fun add_builtin_fun_ext'' n context =
   let val thy = Context.theory_of context
   in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
 
 fun lookup_builtin_fun ctxt =
-  lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt))
+  lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt)))
 
 fun dest_builtin_fun ctxt (c as (_, T)) ts =
   (case lookup_builtin_fun ctxt c of
     SOME (_, Int f) => f ctxt T ts
   | _ => NONE)