src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

   | map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
 
 (* general syntactic functions *)
 
 (*Like dest_conj, but flattens conjunctions however nested*)
-fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
   | conjuncts_aux t conjs = t::conjs;
 
 fun conjuncts t = conjuncts_aux t [];
 
 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
-  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
+  | is_equationlike_term (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
   | is_equationlike_term _ = false
   
 val is_equationlike = is_equationlike_term o prop_of 
 
 fun is_pred_equation_term (Const ("==", _) $ u $ v) =

 
 val is_constr = Code.is_constr o ProofContext.theory_of;
 
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
-fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
+fun strip_ex (Const (@{const_name "Ex"}, _) $ Abs (x, T, t)) =
   let
     val (xTs, t') = strip_ex t
   in
     ((x, T) :: xTs, t')
   end