--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Aug 26 20:51:17 2010 +0200
@@ -198,7 +198,7 @@
| @{term Not} $ _ => abstr1 cvs ct
| @{term "op &"} $ _ $ _ => abstr2 cvs ct
| @{term "op |"} $ _ $ _ => abstr2 cvs ct
- | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
+ | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct