src/HOL/ex/Reflection_Examples.thy

--- a/src/HOL/ex/Reflection_Examples.thy	Fri Feb 15 08:31:31 2013 +0100
+++ b/src/HOL/ex/Reflection_Examples.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -129,7 +129,6 @@
 text {* Now we specify on which subterm it should be applied *}
 lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
   apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
-  apply code_simp
 oops