--- a/src/Pure/ML/ml_context.ML Sat Sep 15 19:25:54 2007 +0200 +++ b/src/Pure/ML/ml_context.ML Sat Sep 15 19:26:06 2007 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/Thy/ml_context.ML +(* Title: Pure/ML/ml_context.ML ID: $Id$ Author: Makarius