# HG changeset patch
# User haftmann
# Date 1272032244 -7200
# Node ID bbcfeddeafbb76412c88c56541b51d889a91a71c
# Parent  1732232f9b27c41b173f5fd321eac6fd96268419
dequalified fact name

diff -r 1732232f9b27 -r bbcfeddeafbb src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 23 15:18:00 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Apr 23 16:17:24 2010 +0200
@@ -33,7 +33,7 @@
              @{thm "real_of_nat_number_of"},
              @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"},
              @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"},
-             @{thm "Fields.divide_zero"}, 
+             @{thm "divide_zero"}, 
              @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
              @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
              @{thm "diff_def"}, @{thm "minus_divide_left"}]