# HG changeset patch
# User wenzelm
# Date 1189877166 -7200
# Node ID 6491d89ba76cd5e37aa5f79ec9edf50c5a95fc80
# Parent  916259859344a2309eb3bf866a232ecfec715058
tuned comments;

diff -r 916259859344 -r 6491d89ba76c src/Pure/ML/ml_context.ML
--- 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