# HG changeset patch
# User wenzelm
# Date 754572489 -3600
# Node ID 793be9f1e88e3ffe4e09436711a618bb3cdc0e4a
# Parent  43506f0a98aec1e56728590b8224159f1b6bce5f
improved comments;

diff -r 43506f0a98ae -r 793be9f1e88e src/Pure/Syntax/sextension.ML
--- a/src/Pure/Syntax/sextension.ML	Mon Nov 29 12:27:29 1993 +0100
+++ b/src/Pure/Syntax/sextension.ML	Mon Nov 29 12:28:09 1993 +0100
@@ -2,8 +2,8 @@
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
-Syntax extensions (external interface): mixfix declarations, syntax rules,
-infixes, binders and the Pure syntax.
+Syntax extensions (external interface): mixfix declarations, infixes,
+binders, translation rules / functions and the Pure syntax.
 
 TODO:
   move ast_to_term (?)