# HG changeset patch
# User wenzelm
# Date 1365506409 -7200
# Node ID 28d6eb23522caa451ef99d2d93dfcc569df017ef
# Parent  8450b944e58a0f705592505493f530f1647b30d5
tuned comment;

diff -r 8450b944e58a -r 28d6eb23522c src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Tue Apr 09 12:56:26 2013 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Tue Apr 09 13:20:09 2013 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Syntax/local_syntax.ML
     Author:     Makarius
 
-Local syntax depending on theory syntax.
+Local syntax depending on theory syntax, with special support for
+implicit structure references.
 *)
 
 signature LOCAL_SYNTAX =