src/HOL/Tools/SMT/z3_proof_tools.ML

         @{term Trueprop} $ _ => abstr1 cvs ct
       | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
       | @{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}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
           else fresh_abstraction cvs ct