# HG changeset patch
# User wenzelm
# Date 1113670673 -7200
# Node ID 65e4790c7914036af5991b7673c0b90f922fb284
# Parent  860c282e6ca63b48365f00d986d898bc317fe820
identify binder translations only once (admits remove);

diff -r 860c282e6ca6 -r 65e4790c7914 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sat Apr 16 18:57:39 2005 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sat Apr 16 18:57:53 2005 +0200
@@ -45,8 +45,7 @@
   val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
 end;
 
-
-structure Mixfix : MIXFIX =
+structure Mixfix: MIXFIX =
 struct
 
 
@@ -158,6 +157,8 @@
 
 (* syn_ext_consts *)
 
+val binder_stamp = stamp ();
+
 fun syn_ext_consts is_logtype const_decls =
   let
     fun name_of (c, _, mx) = const_name c mx;
@@ -192,9 +193,9 @@
     val mfix = List.concat (map mfix_of const_decls);
     val xconsts = map name_of const_decls;
     val binders = List.mapPartial binder const_decls;
-    val binder_trs = map SynTrans.mk_binder_tr binders;
-    val binder_trs' =
-      map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;
+    val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o SynTrans.mk_binder_tr);
+    val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o
+        apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap);
   in
     SynExt.syn_ext' true is_logtype
       mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])