# HG changeset patch
# User haftmann
# Date 1238144708 -3600
# Node ID 9ffd27558916f5c16e067749e369e73a7209e631
# Parent  88bc86d7dec3814562530f5b176cad0067806a02
dropped legacy goal package call

diff -r 88bc86d7dec3 -r 9ffd27558916 src/HOL/Tools/TFL/post.ML
--- 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