src/HOL/Tools/SMT/smt_builtin.ML

   val builtin_fun: Proof.context -> string * typ -> term list ->
     (string * term list) option
   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
   val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
   val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
+  val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
   val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
 end
 
 structure SMT_Builtin: SMT_BUILTIN =
 struct

     get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt))
   end
 
 type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
 
-fun empty_btab () = Symtab.empty
-
 fun insert_btab cs n T f =
   Symtab.map_default (n, []) (insert_ttab cs T f)
 
 fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
 

 
 (* built-in functions *)
 
 type 'a bfun = Proof.context -> typ -> term list -> 'a
 
-fun true3 _ _ _ = true
-
-fun raw_add_builtin_fun_ext thy cs n =
-  insert_btab cs n (Sign.the_const_type thy n) (Ext true3)
-
-val basic_builtin_fun_names = [
-  @{const_name SMT.pat}, @{const_name SMT.nopat},
-  @{const_name SMT.trigger}, @{const_name SMT.weight}]
-
-type builtin_funcs = (bool bfun, (string * term list) option bfun) btab
-
-fun basic_builtin_funcs () : builtin_funcs =
-  empty_btab ()
-  |> fold (raw_add_builtin_fun_ext @{theory} U.basicC) basic_builtin_fun_names
-       (* FIXME: SMT_Normalize should check that they are properly used *)
-
 structure Builtin_Funcs = Generic_Data
 (
-  type T = builtin_funcs
-  val empty = basic_builtin_funcs ()
+  type T = (bool bfun, (string * term list) option bfun) btab
+  val empty = Symtab.empty
   val extend = I
   val merge = merge_btab
 )
 
 fun add_builtin_fun cs ((n, T), f) =

   add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
 
 fun add_builtin_fun_ext ((n, T), f) =
   Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
 
-fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
+fun add_builtin_fun_ext' c =
+  add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)
 
 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