# HG changeset patch
# User haftmann
# Date 1272028679 -7200
# Node ID dbe99291eb3ca2def086faba13176ff0c3b99250
# Parent  6984744e6b3427f4d7e489803f24b9a0c3808812
dequalified fact name

diff -r 6984744e6b34 -r dbe99291eb3c src/HOL/Groebner_Basis.thy
--- 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"},