src/HOL/Tools/SMT/z3_interface.ML

--- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Dec 15 08:39:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Dec 15 10:12:44 2010 +0100
@@ -7,7 +7,6 @@
 signature Z3_INTERFACE =
 sig
   val smtlib_z3C: SMT_Utils.class
-  val interface: SMT_Solver.interface
   val setup: theory -> theory
 
   datatype sym = Sym of string * sym list
@@ -36,8 +35,14 @@
 (* interface *)
 
 local
-  val {translate, extra_norm, ...} = SMTLIB_Interface.interface
-  val {prefixes, is_fol, header, serialize, ...} = translate
+  fun translate_config ctxt =
+    let
+      val {prefixes, header, is_fol, serialize, ...} =
+        SMTLIB_Interface.translate_config ctxt
+    in
+      {prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize,
+        has_datatypes=true}
+    end
 
   fun is_int_div_mod @{const div (int)} = true
     | is_int_div_mod @{const mod (int)} = true
@@ -56,18 +61,10 @@
     B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
 in
 
-val interface = {
-  class = smtlib_z3C,
-  translate = {
-    prefixes = prefixes,
-    is_fol = is_fol,
-    header = header,
-    has_datatypes = true,
-    serialize = serialize}}
-
 val setup = Context.theory_map (
   setup_builtins #>
-  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod))
+  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
+  SMT_Translate.add_config (smtlib_z3C, translate_config))
 
 end
 
@@ -154,11 +151,8 @@
   | mk_distinct (cts as (ct :: _)) =
       Thm.capply (U.instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
 
-val access = U.mk_const_pat @{theory} @{const_name fun_app}
-  (Thm.dest_ctyp o U.destT1)
-fun mk_access array index =
-  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
-  in Thm.mk_binop (U.instTs cTs access) array index end
+val access = U.mk_const_pat @{theory} @{const_name fun_app} U.destT1
+fun mk_access array = Thm.capply (U.instT' array access) array
 
 val update = U.mk_const_pat @{theory} @{const_name fun_upd}
   (Thm.dest_ctyp o U.destT1)
@@ -189,7 +183,7 @@
   | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
   | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
   | (Sym ("distinct", _), _) => SOME (mk_distinct cts)
-  | (Sym ("select", _), [ca, ck]) => SOME (mk_access ca ck)
+  | (Sym ("select", _), [ca, ck]) => SOME (Thm.capply (mk_access ca) ck)
   | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
   | _ =>
     (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of