diff -r 40abbc7c86df -r e98f59806244 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Ring_and_Field.thy	Wed Sep 20 00:24:24 2006 +0200
@@ -241,10 +241,10 @@
 
 instance lordered_ring \<subseteq> lordered_ab_group_join ..
 
-axclass axclass_abs_if \<subseteq> minus, ord, zero
+axclass abs_if \<subseteq> minus, ord, zero
   abs_if: "abs a = (if (a < 0) then (-a) else a)"
 
-axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, axclass_abs_if
+axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, abs_if
 
 instance ordered_ring_strict \<subseteq> lordered_ab_group ..
 
@@ -256,7 +256,7 @@
 axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
   zero_less_one [simp]: "0 < 1"
 
-axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *)
+axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, abs_if (* previously ordered_ring *)
 
 instance ordered_idom \<subseteq> ordered_ring_strict ..