--- a/src/HOL/Hyperreal/HyperBin.ML	Mon Jan 12 14:35:07 2004 +0100
+++ b/src/HOL/Hyperreal/HyperBin.ML	Mon Jan 12 16:45:35 2004 +0100
@@ -344,7 +344,7 @@
 val simplify_meta_eq =
     Int_Numeral_Simprocs.simplify_meta_eq
          [hypreal_add_zero_left, hypreal_add_zero_right,
-          mult_left_zero, mult_right_zero, mult_1, mult_1_right];
+          mult_zero_left, mult_zero_right, mult_1, mult_1_right];
 
 val prep_simproc = Real_Numeral_Simprocs.prep_simproc;