src/Pure/ML/exn_properties_polyml.ML
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;