src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     val cases = map mk_case intros
   in Logic.list_implies (assm :: cases, prop) end;
 
 fun dest_conjunct_prem th =
   case HOLogic.dest_Trueprop (prop_of th) of
-    (Const (@{const_name "op &"}, _) $ t $ t') =>
+    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
       dest_conjunct_prem (th RS @{thm conjunct1})
         @ dest_conjunct_prem (th RS @{thm conjunct2})
     | _ => [th]
 
 fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =