1 (* Title: Pure/Thy/ml_context.ML
1 (* Title: Pure/ML/ml_context.ML
2 ID: $Id$
3 Author: Makarius
4
5 ML context and antiquotations.
6 *)