diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Metis.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -16,7 +16,7 @@
 subsection {* Literal selection and lambda-lifting helpers *}
 
 definition select :: "'a \<Rightarrow> 'a" where
-[no_atp]: "select = (\<lambda>x. x)"
+"select = (\<lambda>x. x)"
 
 lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
 by (cut_tac atomize_not [of "\<not> A"]) simp
@@ -30,7 +30,7 @@
 lemma select_FalseI: "False \<Longrightarrow> select False" by simp
 
 definition lambda :: "'a \<Rightarrow> 'a" where
-[no_atp]: "lambda = (\<lambda>x. x)"
+"lambda = (\<lambda>x. x)"
 
 lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
 unfolding lambda_def by assumption