src/Pure/ML-Systems/smlnj.ML
changeset 14520 af9d7fcf873e
parent 14519 4ca3608fdf4f
child 14656 765badface6a
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Apr 05 13:23:10 2004 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Apr 05 13:30:37 2004 +0200
@@ -46,7 +46,7 @@
   [110, x] => if x >= 45
 	      then use "ML-Systems/cpu-timer-basis.ML"
 	      else use "ML-Systems/cpu-timer-gc.ML"
-| _ => ());
+| _ => use "ML-Systems/cpu-timer-gc.ML");
 
 
 (* prompts *)
@@ -67,7 +67,7 @@
   [110, x] => if x >= 45
 	      then use "ML-Systems/smlnj-pp-new.ML"
 	      else use "ML-Systems/smlnj-pp-old.ML"
-| _ => ());
+| _ => use "ML-Systems/smlnj-pp-old.ML");
 
 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;