diff -r aa6c470a962a -r 560372b461e5 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Oct 15 21:08:03 2009 +0200
+++ b/src/HOL/Predicate.thy	Sat Oct 24 16:54:32 2009 +0200
@@ -770,10 +770,6 @@
    (auto simp add: Seq_def the_only_singleton is_empty_def
       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
 
-lemma meta_fun_cong:
-"f == g ==> f x == g x"
-by simp
-
 ML {*
 signature PREDICATE =
 sig