src/HOL/Complex/NSComplexBin.ML
changeset 14353 79f9fbef9106
parent 14335 9c0b5e081037
child 14373 67a628beb981
--- a/src/HOL/Complex/NSComplexBin.ML	Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Complex/NSComplexBin.ML	Mon Jan 12 16:51:45 2004 +0100
@@ -328,8 +328,7 @@
 val simplify_meta_eq = 
     Int_Numeral_Simprocs.simplify_meta_eq
          [add_zero_left, 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 = Complex_Numeral_Simprocs.prep_simproc;