--- a/src/HOL/Tools/TFL/post.ML Tue Mar 24 23:43:58 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML Fri Mar 27 10:05:08 2009 +0100
@@ -79,10 +79,7 @@
in lhs aconv rhs end
handle U.ERR _ => false;
-
-fun prover s = prove_goal @{theory HOL} s (fn _ => [fast_tac HOL_cs 1]);
-val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
-val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
+val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
Const("==",_)$_$_ => r
| _ $(Const("op =",_)$_$_) => r RS eq_reflection