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 ("op &", _) $ t $ t') =>
+    (Const (@{const_name "op &"}, _) $ 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 =

     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   | _ => Conv.all_conv ct
 
 fun Trueprop_conv cv ct =
   case Thm.term_of ct of
-    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
+    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
   | _ => raise Fail "Trueprop_conv"
 
 fun preprocess_intro thy rule =
   Conv.fconv_rule
     (imp_prems_conv
       (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
     (Thm.transfer thy rule)
 
 fun preprocess_elim ctxt elimrule =
   let
-    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
+    fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
      | replace_eqs t = t
     val thy = ProofContext.theory_of ctxt
     val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
     val prems = Thm.prems_of elimrule