changeset 62077 | e8ae72c26025 |
parent 62076 | 1add21f7cabc |
child 62078 | 76399b8fde4d |
--- a/src/Pure/RAW/polyml-5.6.ML Wed Jan 06 10:08:09 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* Title: Pure/RAW/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/polyml.ML";