diff -r 3298b7a2795a -r 84fc7dfa3cd4 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -199,7 +199,7 @@
     and abstr (dcvs as (d, cvs)) ct =
       (case Thm.term_of ct of
         @{const Trueprop} $ _ => abstr1 dcvs ct
-      | @{const "==>"} $ _ $ _ => abstr2 dcvs ct
+      | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct
       | @{const True} => pair ct
       | @{const False} => pair ct
       | @{const Not} $ _ => abstr1 dcvs ct
@@ -229,7 +229,7 @@
             | _ => fresh_abstraction dcvs ct cx)))
   in abstr (depth, []) end
 
-val cimp = Thm.cterm_of @{theory} @{const "==>"}
+val cimp = Thm.cterm_of @{theory} @{const Pure.imp}
 
 fun deepen depth f x =
   if depth = 0 then f depth x