diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NSA/Examples/NSPrimes.thy
--- a/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -39,7 +39,7 @@
 apply (force intro!: dvd_mult)
 done
 
-lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
+lemmas dvd_by_all2 = dvd_by_all [THEN spec]
 
 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
 by (transfer, simp)
@@ -50,7 +50,7 @@
 lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
 by (transfer, rule dvd_by_all)
 
-lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
+lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]
 
 (* Goldblatt: Exercise 5.11(2) - p. 57 *)
 lemma hypnat_dvd_all_hypnat_of_nat: