diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -175,7 +175,7 @@
   done
 
 lemma B_greater_zero: "x \<in> B ==> 0 < x"
-  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
+  using a_nonzero by (auto simp add: B_def A_greater_zero)
 
 lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   apply (auto simp add: C_def)