# HG changeset patch
# User berghofe
# Date 1008952305 -3600
# Node ID dceea9dbdeddb7031e54ab7b9bac9f4df977c384
# Parent  7fdc00bb2a9e23d910236106cde5c557ecc18ea2
Redundant patterns no longer cause errors.

diff -r 7fdc00bb2a9e -r dceea9dbdedd src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Dec 21 17:31:08 2001 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Fri Dec 21 17:31:45 2001 +0100
@@ -21,7 +21,8 @@
  (Compiler.Control.Print.printLength := 1000;
   Compiler.Control.Print.printDepth := 350;
   Compiler.Control.Print.stringDepth := 250;
-  Compiler.Control.Print.signatures := 2);
+  Compiler.Control.Print.signatures := 2;
+  Compiler.Control.MC.matchRedundantError := false);
 
 
 (* Poly/ML emulation *)