specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

--- a/src/HOL/Record.thy	Mon May 07 14:50:49 2012 +0200
+++ b/src/HOL/Record.thy	Tue May 08 14:31:03 2012 +0200
@@ -400,7 +400,7 @@
 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   by simp
 
-lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
+lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
   by simp
 
 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"