src/Pure/General/ml_syntax.ML
changeset 24369 0cb1f4d76452
parent 22716 85f0ab03eeed