--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Aug 27 10:56:46 2010 +0200
@@ -216,8 +216,8 @@
(Sym ("true", _), []) => SOME mk_true
| (Sym ("false", _), []) => SOME mk_false
| (Sym ("not", _), [ct]) => SOME (mk_not ct)
- | (Sym ("and", _), _) => SOME (mk_nary @{cterm "op &"} mk_true cts)
- | (Sym ("or", _), _) => SOME (mk_nary @{cterm "op |"} mk_false cts)
+ | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
+ | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)