src/Pure/RAW/ROOT_polyml-5.5.2.ML
changeset 62461 075ef5ec115c
parent 62458 9590972c2caf
parent 62460 4b2018eb92e8
child 62462 c7def2433a06
child 62464 08e62096e7f4
--- a/src/Pure/RAW/ROOT_polyml-5.5.2.ML	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_polyml-5.5.2.ML
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML 5.5.2.
-*)
-
-structure Thread =
-struct
-  open Thread;
-
-  structure Thread =
-  struct
-    open Thread;
-
-    fun numProcessors () =
-      (case Thread.numPhysicalProcessors () of
-        SOME n => n
-      | NONE => Thread.numProcessors ());
-  end;
-end;
-
-use "RAW/ROOT_polyml.ML";
-