diff -r eb8b8241ef5b -r 8dbbb7cf3637 src/HOL/Hyperreal/HRealAbs.ML
--- a/src/HOL/Hyperreal/HRealAbs.ML	Thu Dec 25 23:18:04 2003 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML	Sat Dec 27 21:02:14 2003 +0100
@@ -105,7 +105,7 @@
 by (asm_full_simp_tac (simpset() addsimps [hrabs_def] 
                                  addsplits [split_if_asm]) 2); 
 by (case_tac "y = 0" 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_mult_iff]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1); 
 by (rtac hypreal_mult_less_mono 1); 
 by (auto_tac (claset(), 
               simpset() addsimps [hrabs_def, linorder_neq_iff]