--- a/src/HOL/Tools/SMT/z3_model.ML Thu May 27 14:58:45 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_model.ML Thu May 27 16:29:33 2010 +0200
@@ -122,7 +122,7 @@
| trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
-fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u
+fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u
| mk_eq t (us, u) = mk_eq' t us u
fun translate (t, cs) =