diff -r 6d1ecdb81ff0 -r 8e55aa1306c5 src/HOL/SMT/Tools/z3_interface.ML
--- a/src/HOL/SMT/Tools/z3_interface.ML	Wed May 12 23:54:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      HOL/SMT/Tools/z3_interface.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Interface to Z3 based on a relaxed version of SMT-LIB.
-*)
-
-signature Z3_INTERFACE =
-sig
-  val interface: string list -> SMT_Translate.config
-end
-
-structure Z3_Interface: Z3_INTERFACE =
-struct
-
-fun z3_builtin_fun bf c ts =
-  (case Const c of
-    @{term "op / :: real => _"} => SOME ("/", ts)
-  | _ => bf c ts)
-
-fun interface comments =
-  let
-    val {prefixes, strict, builtins, serialize} =
-      SMTLIB_Interface.interface comments
-    val {builtin_typ, builtin_num, builtin_fun} = builtins
-  in
-   {prefixes = prefixes,
-    strict = strict,
-    builtins = {
-      builtin_typ = builtin_typ,
-      builtin_num = builtin_num,
-      builtin_fun = z3_builtin_fun builtin_fun},
-    serialize = serialize}
-  end
-
-end