# HG changeset patch
# User wenzelm
# Date 777303356 -7200
# Node ID 4c139c37dbafff4a4fc96593afb3577a3d42ddf1
# Parent  353eea6ec2321dceb882340bbf17968e952616e6
minor cleanings;

diff -r 353eea6ec232 -r 4c139c37dbaf src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Aug 19 15:35:38 1994 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Aug 19 15:35:56 1994 +0200
@@ -1,13 +1,8 @@
 (*  Title:      Pure/Syntax/mixfix.ML
     ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Mixfix declarations, infixes, binders. Part of the Pure syntax.
-
-TODO:
-  note: needs mk_binder_tr/tr'
-  Mixfix.mixfix -> mixfix
-  remove ....Mixfix
 *)
 
 signature MIXFIX0 =
@@ -42,11 +37,11 @@
 end;
 
 functor MixfixFun(structure Lexicon: LEXICON and SynExt: SYN_EXT
-  and SExtension: SEXTENSION): MIXFIX =
+  and SynTrans: SYN_TRANS): MIXFIX =
 struct
 
 structure SynExt = SynExt;
-open Lexicon SynExt SynExt.Ast SExtension;
+open Lexicon SynExt SynExt.Ast SynTrans;
 
 
 (** mixfix declarations **)