diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Proofs/Lambda/NormalForm.thy
--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -132,10 +132,10 @@
   apply (drule listall_conj2)
   apply (drule_tac i=i and j=j in subst_terms_NF)
   apply assumption
-  apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])
+  apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
   apply simp
   apply (erule NF.App)
-  apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
+  apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
   apply simp
   apply (iprover intro: NF.App)
   apply simp
@@ -173,7 +173,7 @@
   apply (drule listall_conj2)
   apply (drule_tac i=i in lift_terms_NF)
   apply assumption
-  apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])
+  apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
   apply simp
   apply (rule NF.App)
   apply assumption