src/HOL/Statespace/distinct_tree_prover.ML

     val thm = distinctTreeProver dist_thm x_path y_path;
   in SOME thm  
   end handle Option => NONE)
 
 fun distinctTree_tac names ctxt 
-      (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
+      (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
   (case get_fst_success (neq_x_y ctxt x y) names of
      SOME neq => rtac neq i
    | NONE => no_tac)
   | distinctTree_tac _ _ _ = no_tac;
 

                  SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
                 | NONE => fn i => no_tac)
 
 fun distinct_simproc names =
   Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
-    (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
+    (fn thy => fn ss => fn (Const (@{const_name "op ="},_)$x$y) =>
         case try Simplifier.the_context ss of
         SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
                       (get_fst_success (neq_x_y ctxt x y) names)
        | NONE => NONE
     )