src/Pure/General/ml_syntax.ML
changeset 24066 fb455cb475df
parent 22716 85f0ab03eeed