src/HOL/NSA/Examples/NSPrimes.thy

--- a/src/HOL/NSA/Examples/NSPrimes.thy	Wed Mar 11 11:21:58 2015 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Thu Mar 12 14:08:47 2015 +0100
@@ -13,8 +13,6 @@
 text{*These can be used to derive an alternative proof of the infinitude of
 primes by considering a property of nonstandard sets.*}
 
-declare dvd_def [transfer_refold]
-
 definition
   starprime :: "hypnat set" where
   [transfer_unfold]: "starprime = ( *s* {p. prime p})"