src/HOL/Record.thy

--- a/src/HOL/Record.thy	Thu Oct 01 00:32:00 2009 +0200
+++ b/src/HOL/Record.thy	Thu Oct 01 01:03:36 2009 +0200
@@ -450,10 +450,6 @@
   "Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)"
   by simp
 
-lemma meta_all_sameI:
-  "(\<And>x. PROP P x \<equiv> PROP Q x) \<Longrightarrow> (\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)"
-  by simp
-
 lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
   by simp