# HG changeset patch
# User blanchet
# Date 1380550076 -7200
# Node ID b352d3d4a58a928720c362490b2dc71058487017
# Parent  8ff43f638da233fedfb8d28bec61479910d7bb96
just one data slot (record) per program unit

diff -r 8ff43f638da2 -r b352d3d4a58a src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Sep 30 15:10:18 2013 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Mon Sep 30 16:07:56 2013 +0200
@@ -91,27 +91,30 @@
     NONE => NONE
   | SOME ttab => lookup_ttab ctxt ttab T)
 
+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 *
+    (term list bfun, bfunr option bfun) btab
+  val empty = ([], Symtab.empty)
+  val extend = I
+  fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
+)
 
 (* built-in types *)
 
-(* FIXME just one data slot (record) per program unit *)
-structure Builtin_Types = Generic_Data
-(
-  type T =
-    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
-  val empty = []
-  val extend = I
-  val merge = merge_ttab
-)
-
 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
@@ -145,21 +148,8 @@
 
 (* 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
@@ -169,7 +159,7 @@
   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)
 
@@ -178,7 +168,7 @@
   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