diff -r e33519ec9e91 -r faf62905cd53 src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Thu Mar 01 21:35:49 2012 +0100
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Fri Mar 02 09:35:32 2012 +0100
@@ -67,10 +67,7 @@
 subsection {* Basic Properties of the Gauss Sets *}
 
 lemma finite_A: "finite (A)"
-  apply (auto simp add: A_def)
-  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
-  apply (auto simp add: bdd_int_set_l_finite finite_subset)
-  done
+by (auto simp add: A_def)
 
 lemma finite_B: "finite (B)"
 by (auto simp add: B_def finite_A)