Redundant patterns no longer cause errors.
authorberghofe
Fri, 21 Dec 2001 17:31:45 +0100
changeset 12581dceea9dbdedd
parent 12580 7fdc00bb2a9e
child 12582 b85acd66f715
Redundant patterns no longer cause errors.
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Dec 21 17:31:08 2001 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Fri Dec 21 17:31:45 2001 +0100
     1.3 @@ -21,7 +21,8 @@
     1.4   (Compiler.Control.Print.printLength := 1000;
     1.5    Compiler.Control.Print.printDepth := 350;
     1.6    Compiler.Control.Print.stringDepth := 250;
     1.7 -  Compiler.Control.Print.signatures := 2);
     1.8 +  Compiler.Control.Print.signatures := 2;
     1.9 +  Compiler.Control.MC.matchRedundantError := false);
    1.10  
    1.11  
    1.12  (* Poly/ML emulation *)