# HG changeset patch
# User wenzelm
# Date 1138144897 -3600
# Node ID a9f41c380b2f4603e366f2090bbfe6c3a8c2f42e
# Parent  f623f7a35cedae074be79ff4b00f94f905e80aaf
tuned comment;

diff -r f623f7a35ced -r a9f41c380b2f src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed Jan 25 00:21:36 2006 +0100
+++ b/src/Pure/Isar/constdefs.ML	Wed Jan 25 00:21:37 2006 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
 
-Standard constant definitions, with type-inference and optional
+Old-style constant definitions, with type-inference and optional
 structure context; specifications need to observe strictly sequential
 dependencies; no support for overloading.
 *)