diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -42,10 +42,10 @@
               Int_assoc [symmetric])
 
 (* [| F \<in> Always C;  F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
-lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
+lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1]
 
 (* [| F \<in> Always INV;  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
-lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
+lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2]
 
 
 subsection{*Introduction rules: Basis, Trans, Union*}
@@ -104,7 +104,7 @@
 apply (blast intro: subset_imp_leadsTo)
 done
 
-lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
+lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, simp]
 
 lemma LeadsTo_weaken_R:
      "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"