diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Induct/PropLog.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -111,7 +111,7 @@
 
 lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
 
-lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
+lemmas thms_notE = thms.MP [THEN thms_falseE]
 
 
 subsubsection {* Soundness of the rules wrt truth-table semantics *}