--- a/src/HOL/HOL.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/HOL.thy Sun Nov 20 21:07:10 2011 +0100
@@ -494,7 +494,7 @@
apply assumption
done
-lemmas ccontr = FalseE [THEN classical, standard]
+lemmas ccontr = FalseE [THEN classical]
(*notE with premises exchanged; it discharges ~R so that it can be used to
make elimination rules*)
@@ -1445,8 +1445,8 @@
lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
lemmas induct_atomize = induct_atomize' induct_equal_eq
-lemmas induct_rulify' [symmetric, standard] = induct_atomize'
-lemmas induct_rulify [symmetric, standard] = induct_atomize
+lemmas induct_rulify' [symmetric] = induct_atomize'
+lemmas induct_rulify [symmetric] = induct_atomize
lemmas induct_rulify_fallback =
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_true_def induct_false_def