src/HOL/Tools/SMT2/smt2_util.ML

 fun dest_cprop ct =
   (case Thm.term_of ct of
     @{const Trueprop} $ _ => Thm.dest_arg ct
   | _ => raise CTERM ("not a property", [ct]))
 
-val equals = mk_const_pat @{theory} @{const_name "=="} destT1
+val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
 
 val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
 fun term_of ct = dest_prop (Thm.term_of ct)
 fun prop_of thm = dest_prop (Thm.prop_of thm)