diff -r 375db037f4d2 -r 341c83339aeb src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Sat Aug 29 14:31:39 2009 +0200
+++ b/src/HOL/Library/Continuity.thy	Mon Aug 31 14:09:42 2009 +0200
@@ -156,7 +156,7 @@
  apply (rule up_chainI)
  apply simp
 apply (drule Un_absorb1)
-apply (auto simp add: nat_not_singleton)
+apply (auto split:split_if_asm)
 done
 
 
@@ -184,8 +184,7 @@
  apply (rule down_chainI)
  apply simp
 apply (drule Int_absorb1)
-apply auto
-apply (auto simp add: nat_not_singleton)
+apply (auto split:split_if_asm)
 done