--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Aug 27 10:56:46 2010 +0200
@@ -196,8 +196,8 @@
| @{term True} => pair ct
| @{term False} => pair ct
| @{term Not} $ _ => abstr1 cvs ct
- | @{term "op &"} $ _ $ _ => abstr2 cvs ct
- | @{term "op |"} $ _ $ _ => abstr2 cvs ct
+ | @{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 distinct}, _) $ _ =>