src/HOL/Tools/SMT/z3_interface.ML

 fun mk_builtin_fun ctxt sym cts =
   (case (sym, cts) of
     (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)
   | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu))
   | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)