changeset 62464 | 08e62096e7f4 |
parent 62463 | 547c5c6e66d4 |
parent 62461 | 075ef5ec115c |
child 62465 | 2e4c6ef809b5 |
--- a/src/Pure/RAW/ROOT_polyml-5.5.2.ML Mon Feb 29 11:42:15 2016 +0000 +++ /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"; -