src/Pure/ML-Systems/smlnj.ML
changeset 12581 dceea9dbdedd
parent 12108 b6f10dcde803
child 12874 368966ceafe5
     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 *)