# 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"},