diff -r 053c69cb4a0e -r 4abe644fcea5 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -199,7 +199,7 @@
       | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
       | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
       | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
-      | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
+      | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
           else fresh_abstraction cvs ct