src/HOL/Tools/TFL/post.ML

--- a/src/HOL/Tools/TFL/post.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -63,7 +63,7 @@
    
 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