diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 15:45:42 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 15:45:43 2010 +0100
@@ -13,6 +13,9 @@
 structure Z3_Model: Z3_MODEL =
 struct
 
+structure U = SMT_Utils
+
+
 (* counterexample expressions *)
 
 datatype expr = True | False | Number of int * int option | Value of int |
@@ -214,15 +217,13 @@
 
 fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
 
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
 fun mk_update ([], u) _ = u
   | mk_update ([t], u) f =
-      uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
+      uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
   | mk_update (t :: ts, u) f =
       let
-        val (dT, rT) = split_type (Term.fastype_of f)
-        val (dT', rT') = split_type rT
+        val (dT, rT) = U.split_type (Term.fastype_of f)
+        val (dT', rT') = U.split_type rT
       in
         mk_fun_upd dT rT $ f $ t $
           mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))