removed unused file smt_builtin.ML,
made negative pattern polymorphic (similar to positve pattern)

--- a/src/HOL/IsaMakefile	Tue Oct 27 18:01:50 2009 +0100
+++ b/src/HOL/IsaMakefile	Tue Oct 27 18:09:11 2009 +0100
@@ -1187,12 +1187,11 @@
 
 $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy		\
   SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML	\
-  SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML			\
-  SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML			\
-  SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML			\
-  SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML		\
-  SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML				\
-  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
+  SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML              \
+  SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML                      \
+  SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML                 \
+  SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML                     \
+  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
 
 

--- a/src/HOL/SMT/SMT_Base.thy	Tue Oct 27 18:01:50 2009 +0100
+++ b/src/HOL/SMT/SMT_Base.thy	Tue Oct 27 18:09:11 2009 +0100
@@ -29,7 +29,7 @@
 definition pat :: "'a \<Rightarrow> pattern"
 where "pat _ = Pattern"
 
-definition nopat :: "bool \<Rightarrow> pattern"
+definition nopat :: "'a \<Rightarrow> pattern"
 where "nopat _ = Pattern"
 
 definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)

--- a/src/HOL/SMT/Tools/smt_builtin.ML	Tue Oct 27 18:01:50 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      HOL/SMT/Tools/smt_builtin.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Tables for built-in symbols.
-*)
-
-signature SMT_BUILTIN =
-sig
-  type sterm = (SMT_Translate.sym, typ) sterm
-  type builtin_fun = typ -> sterm list -> (string * sterm list) option
-  type table = (typ * builtin_fun) list Symtab.table
-
-  val make: (term * string) list -> table
-  val add: term * builtin_fun -> table -> table
-  val lookup: table -> theory -> string * typ -> sterm list ->
-    (string * sterm list) option
-
-  val bv_rotate: (int -> string) -> builtin_fun
-  val bv_extend: (int -> string) -> builtin_fun
-  val bv_extract: (int -> int -> string) -> builtin_fun
-end
-
-structure SMT_Builtin: SMT_BUILTIN =
-struct
-
-structure T = SMT_Translate
-
-type sterm = (SMT_Translate.sym, typ) sterm
-type builtin_fun = typ -> sterm list -> (string * sterm list) option
-type table = (typ * builtin_fun) list Symtab.table
-
-fun make entries =
-  let
-    fun dest (t, bn) =
-      let val (n, T) = Term.dest_Const t
-      in (n, (Logic.varifyT T, K (pair bn))) end
-  in Symtab.make (AList.group (op =) (map dest entries)) end
-
-fun add (t, f) tab =
-  let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
-  in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
-
-fun lookup tab thy (n, T) =
-  AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T
-
-
-fun dest_binT T =
-  (case T of
-    Type (@{type_name "Numeral_Type.num0"}, _) => 0
-  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
-  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
-  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
-  | _ => raise TYPE ("dest_binT", [T], []))
-
-fun dest_wordT T =
-  (case T of
-    Type (@{type_name "word"}, [T]) => dest_binT T
-  | _ => raise TYPE ("dest_wordT", [T], []))
-
-
-val dest_nat = (fn
-    SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
-  | _ => NONE)
-
-fun bv_rotate mk_name T ts =
-  dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
-
-fun bv_extend mk_name T ts =
-  (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
-    (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
-  | _ => NONE)
-
-fun bv_extract mk_name T ts =
-  (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
-    (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
-  | _ => NONE)
-
-end