Promote more Isabelle concurrency code

Portable gets slightly richer with

make_counter : {inc:int,init:int} -> unit -> int
syncref : 'a -> {get:unit->'a, upd : ('a -> 'b * 'a) -> 'b}

Under Moscow ML these map to obvious operations on references. Under
Poly/ML these map to synchronised variables that are operated on
atomically.