src/Pure/Syntax/mixfix.ML
changeset 21534 68f805e9db0b
parent 20892 318f0ff93d99
child 21805 6af1aa7f67d6
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sun Nov 26 18:07:31 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sun Nov 26 18:07:33 2006 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4      Infixr of int |   (*obsolete*)
     1.5      Binder of string * int * int |
     1.6      Structure
     1.7 +  val binder_name: string -> string
     1.8  end;
     1.9  
    1.10  signature MIXFIX1 =
    1.11 @@ -186,6 +187,7 @@
    1.12  (* syn_ext_consts *)
    1.13  
    1.14  val binder_stamp = stamp ();
    1.15 +val binder_name = suffix "_binder";
    1.16  
    1.17  fun syn_ext_consts is_logtype const_decls =
    1.18    let
    1.19 @@ -212,11 +214,11 @@
    1.20          | (sy, ty, Infixl p) => mk_infix sy ty c p (p + 1) p
    1.21          | (sy, ty, Infixr p) => mk_infix sy ty c (p + 1) p p
    1.22          | (_, ty, Binder (sy, p, q)) =>
    1.23 -            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)]
    1.24 +            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
    1.25          | _ => error ("Bad mixfix declaration for const: " ^ quote c))
    1.26      end;
    1.27  
    1.28 -    fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c)
    1.29 +    fun binder (c, _, Binder _) = SOME (binder_name c, c)
    1.30        | binder _ = NONE;
    1.31  
    1.32      val mfix = maps mfix_of const_decls;