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 =