--- a/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 21 03:56:51 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 21 04:33:17 2010 +0100
@@ -41,7 +41,6 @@
val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
val is_builtin_fun: 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 =
@@ -219,8 +218,4 @@
| SOME (_, Ext f) => f ctxt T ts
| NONE => false)
-fun is_builtin_ext ctxt c ts =
- is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse
- is_builtin_fun_ext ctxt c ts
-
end