Changes

Summary

tuned, centralizing case distinction at one place at the cost of modest duplication

Changeset 75397:e852c776a455 by haftmann: tuned, centralizing case distinction at one place at the cost of modest duplication
The file was modified	`src/Tools/Code/code_thingol.ML` (diff)