src/HOL/Tools/TFL/post.ML

    in lhs aconv rhs end
    handle Utils.ERR _ => false;
    
 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
 fun mk_meta_eq r = case concl_of r of
-     Const("==",_)$_$_ => r
+     Const(@{const_name Pure.eq},_)$_$_ => r
   |   _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
   |   _ => r RS P_imp_P_eq_True
 
 (*Is this the best way to invoke the simplifier??*)
 fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))