diff -r 00f311c32444 -r 9f841f20dca6 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Mon Feb 08 17:12:32 2010 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp	Mon Feb 08 17:12:38 2010 +0100
@@ -162,12 +162,12 @@
   "LESS_OR" > "Nat.Suc_leI"
   "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
   "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
-  "LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
+  "LESS_MULT2" > "Rings.mult_pos_pos"
   "LESS_MONO_REV" > "Nat.Suc_less_SucD"
   "LESS_MONO_MULT" > "Nat.mult_le_mono1"
   "LESS_MONO_EQ" > "Nat.Suc_less_eq"
-  "LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
-  "LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
+  "LESS_MONO_ADD_INV" > "Groups.add_less_imp_less_right"
+  "LESS_MONO_ADD_EQ" > "Groups.add_less_cancel_right"
   "LESS_MONO_ADD" > "Nat.add_less_mono1"
   "LESS_MOD" > "Divides.mod_less"
   "LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
@@ -180,7 +180,7 @@
   "LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
   "LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
   "LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
-  "LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
+  "LESS_EQ_MONO_ADD_EQ" > "Groups.add_le_cancel_right"
   "LESS_EQ_MONO" > "Nat.Suc_le_mono"
   "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
   "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"