diff -r 0a2371e7ced3 -r 0ede9e2266a8 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