# HG changeset patch
# User wenzelm
# Date 1164560853 -3600
# Node ID 68f805e9db0bbee9b2491502d2e960e04a3d317d
# Parent  bada5ac1216a50dc6f9b65840fd2d9bdf871125c
Binder: syntax const is determined by binder_name, not its syntax;

diff -r bada5ac1216a -r 68f805e9db0b src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sun Nov 26 18:07:31 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Sun Nov 26 18:07:33 2006 +0100
@@ -19,6 +19,7 @@
     Infixr of int |   (*obsolete*)
     Binder of string * int * int |
     Structure
+  val binder_name: string -> string
 end;
 
 signature MIXFIX1 =
@@ -186,6 +187,7 @@
 (* syn_ext_consts *)
 
 val binder_stamp = stamp ();
+val binder_name = suffix "_binder";
 
 fun syn_ext_consts is_logtype const_decls =
   let
@@ -212,11 +214,11 @@
         | (sy, ty, Infixl p) => mk_infix sy ty c p (p + 1) p
         | (sy, ty, Infixr p) => mk_infix sy ty c (p + 1) p p
         | (_, ty, Binder (sy, p, q)) =>
-            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)]
+            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
         | _ => error ("Bad mixfix declaration for const: " ^ quote c))
     end;
 
-    fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c)
+    fun binder (c, _, Binder _) = SOME (binder_name c, c)
       | binder _ = NONE;
 
     val mfix = maps mfix_of const_decls;