src/Pure/ML-Systems/smlnj.ML
changeset 14520 af9d7fcf873e
parent 14519 4ca3608fdf4f
child 14656 765badface6a
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Apr 05 13:23:10 2004 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Apr 05 13:30:37 2004 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4    [110, x] => if x >= 45
     1.5  	      then use "ML-Systems/cpu-timer-basis.ML"
     1.6  	      else use "ML-Systems/cpu-timer-gc.ML"
     1.7 -| _ => ());
     1.8 +| _ => use "ML-Systems/cpu-timer-gc.ML");
     1.9  
    1.10  
    1.11  (* prompts *)
    1.12 @@ -67,7 +67,7 @@
    1.13    [110, x] => if x >= 45
    1.14  	      then use "ML-Systems/smlnj-pp-new.ML"
    1.15  	      else use "ML-Systems/smlnj-pp-old.ML"
    1.16 -| _ => ());
    1.17 +| _ => use "ML-Systems/smlnj-pp-old.ML");
    1.18  
    1.19  fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
    1.20