#3378: Remove deprecated Symbol(dummy=True) syntax

and some cleanup for risch.py