--- a/src/HOL/Groebner_Basis.thy Fri Apr 23 15:17:59 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy Fri Apr 23 15:17:59 2010 +0200
@@ -627,7 +627,7 @@
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
@{thm "divide_Numeral1"},
- @{thm "Fields.divide_zero"}, @{thm "divide_Numeral0"},
+ @{thm "divide_zero"}, @{thm "divide_Numeral0"},
@{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
@{thm "mult_num_frac"}, @{thm "mult_frac_num"},
@{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},