changeset 62512 | 922e702ae8ca |
parent 62500 | ff99681b3fd8 |
parent 62511 | 93fa1efc7219 |
child 62513 | 702085ca8564 |
--- a/src/Pure/RAW/ROOT_polyml-5.6.ML Thu Mar 03 17:03:09 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* Title: Pure/RAW/ROOT_polyml-5.6.ML - Author: Makarius - -Compatibility wrapper for Poly/ML 5.6. -*) - -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";