# HG changeset patch
# User wenzelm
# Date 1292932127 -3600
# Node ID 04ecd79827f29b4131991608946ae5b312e10758
# Parent  8d9b73ef5eae331bec9b82de9e14a5c1acd5b354# Parent  684003dbda540953e4db88debfc88c4fce1243a5
merged

diff -r 684003dbda54 -r 04ecd79827f2 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 21 01:12:14 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 21 12:48:47 2010 +0100
@@ -27,8 +27,8 @@
     (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
   val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
     Context.generic
-  val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
-    Context.generic
+  val add_builtin_fun_ext: (string * typ) * term list bfun ->
+    Context.generic -> Context.generic
   val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
   val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
   val dest_builtin_fun: Proof.context -> string * typ -> term list ->
@@ -39,6 +39,8 @@
   val dest_builtin_conn: Proof.context -> string * typ -> term list ->
     bfunr option
   val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
+  val dest_builtin_ext: Proof.context -> string * typ -> term list ->
+    term list option
   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
   val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
 end
@@ -148,7 +150,7 @@
 
 structure Builtin_Funcs = Generic_Data
 (
-  type T = (bool bfun, bfunr option bfun) btab
+  type T = (term list bfun, bfunr option bfun) btab
   val empty = Symtab.empty
   val extend = I
   val merge = merge_btab
@@ -167,8 +169,7 @@
 fun add_builtin_fun_ext ((n, T), f) =
   Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f))
 
-fun add_builtin_fun_ext' c =
-  add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true)
+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
@@ -210,12 +211,18 @@
     | NONE => dest_builtin_fun ctxt c ts)
   end
 
+fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =    
+  (case lookup_builtin_fun ctxt c of
+    SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
+  | SOME (_, Ext f) => SOME (f ctxt T ts)
+  | NONE => NONE)
+
+fun dest_builtin_ext ctxt c ts =
+  if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
+  else dest_builtin_fun_ext ctxt c ts
+
 fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
 
-fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
-  (case lookup_builtin_fun ctxt c of
-    SOME (_, Int f) => is_some (f ctxt T ts)
-  | SOME (_, Ext f) => f ctxt T ts
-  | NONE => false)
+fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
 
 end