src/Pure/ML-Systems/smlnj.ML
changeset 14656 765badface6a
parent 14520 af9d7fcf873e
child 14981 e73f8140af78
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Apr 22 12:19:40 2004 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Apr 22 12:31:33 2004 +0200
@@ -43,7 +43,7 @@
 (* compiler-independent timing functions *)
 
 (case #version_id (Compiler.version) of
-  [110, x] => if x >= 45
+  [110, x] => if x >= 44
 	      then use "ML-Systems/cpu-timer-basis.ML"
 	      else use "ML-Systems/cpu-timer-gc.ML"
 | _ => use "ML-Systems/cpu-timer-gc.ML");
@@ -56,7 +56,7 @@
 
 
 (case #version_id (Compiler.version) of
-  [110, x] => if x >= 45
+  [110, x] => if x >= 44
 	      then use "ML-Systems/smlnj-basis-compat.ML"
 	      else ()
 | _ => ());
@@ -64,7 +64,7 @@
 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
 
 (case #version_id (Compiler.version) of
-  [110, x] => if x >= 45
+  [110, x] => if x >= 44
 	      then use "ML-Systems/smlnj-pp-new.ML"
 	      else use "ML-Systems/smlnj-pp-old.ML"
 | _ => use "ML-Systems/smlnj-pp-old.ML");