Redundant patterns no longer cause errors.
authorberghofe
Fri, 21 Dec 2001 17:31:45 +0100
changeset 12581 dceea9dbdedd
parent 12580 7fdc00bb2a9e
child 12582 b85acd66f715
Redundant patterns no longer cause errors.
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 *)