src/HOL/Record.thy

--- a/src/HOL/Record.thy	Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Record.thy	Fri Oct 18 10:43:20 2013 +0200
@@ -399,7 +399,7 @@
 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   by simp
 
-lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
+lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
   by simp
 
 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"