--- a/src/HOLCF/IOA/NTP/Impl.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -61,7 +61,7 @@
 
 subsection {* Invariants *}
 
-declare Let_def [simp] le_SucI [simp]
+declare le_SucI [simp]
 
 lemmas impl_ioas =
   impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection]