src/HOL/Decision_Procs/ferrante_rackoff.ML

    (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi,
               ld = ld, qe = qe, atoms = atoms},
              {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
 let
  fun uset (vars as (x::vs)) p = case term_of p of
-   Const(@{const_name "op &"}, _)$ _ $ _ =>
+   Const(@{const_name HOL.conj}, _)$ _ $ _ =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
      in (lS@rS, Drule.binop_cong_rule b lth rth) end
- |  Const(@{const_name "op |"}, _)$ _ $ _ =>
+ |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
      let
        val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
        val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
      in (lS@rS, Drule.binop_cong_rule b lth rth) end
  | _ =>

    val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
         ld_le, ld_gt, ld_ge, ld_P] = map (instantiate ([],[(U_v,cU)])) ld
 
    fun decomp_mpinf fm =
      case term_of fm of
-       Const(@{const_name "op &"},_)$_$_ =>
+       Const(@{const_name HOL.conj},_)$_$_ =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
                          (Thm.cabs x p) (Thm.cabs x q))
         end
-     | Const(@{const_name "op |"},_)$_$_ =>
+     | Const(@{const_name HOL.disj},_)$_$_ =>
         let val (p,q) = Thm.dest_binop fm
         in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
                          (Thm.cabs x p) (Thm.cabs x q))
         end
      | _ =>

        if domain_type T = HOLogic.boolT then find_args bounds tm
        else Thm.dest_fun2 tm
    | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
-   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)