# HG changeset patch
# User wenzelm
# Date 850494562 -3600
# Node ID d00e6f44df79dd8088c6a01acd7c2e515a9cc846
# Parent  90280b3a538b6806b372fe8197b508de40085c45
binder_tr': applied fix_tr';

diff -r 90280b3a538b -r d00e6f44df79 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Dec 13 12:01:26 1996 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 13 17:29:22 1996 +0100
@@ -144,7 +144,7 @@
     val xconsts = map name_of const_decls;
     val binders = mapfilter binder const_decls;
     val binder_trs = map mk_binder_tr binders;
-    val binder_trs' = map (mk_binder_tr' o swap) binders;
+    val binder_trs' = map (apsnd fix_tr' o mk_binder_tr' o swap) binders;
   in
     syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
   end;