canonical argument order for type_name, const_name;
authorwenzelm
Sat Mar 07 21:20:17 2009 +0100 (2009-03-07)
changeset 3034060b2c50420d2
parent 30339 3fc32dd7a647
child 30341 78d08e2d01b9
canonical argument order for type_name, const_name;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sat Mar 07 21:19:24 2009 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat Mar 07 21:20:17 2009 +0100
     1.3 @@ -27,8 +27,8 @@
     1.4    val literal: string -> mixfix
     1.5    val no_syn: 'a * 'b -> 'a * 'b * mixfix
     1.6    val pretty_mixfix: mixfix -> Pretty.T
     1.7 -  val type_name: string -> mixfix -> string
     1.8 -  val const_name: string -> mixfix -> string
     1.9 +  val type_name: mixfix -> string -> string
    1.10 +  val const_name: mixfix -> string -> string
    1.11    val const_mixfix: string -> mixfix -> string * mixfix
    1.12    val mixfix_args: mixfix -> int
    1.13    val mixfixT: mixfix -> typ
    1.14 @@ -105,28 +105,28 @@
    1.15  
    1.16  fun deprecated c = (legacy_feature ("Unnamed infix operator " ^ quote c); c);
    1.17  
    1.18 -fun type_name t (InfixName _) = t
    1.19 -  | type_name t (InfixlName _) = t
    1.20 -  | type_name t (InfixrName _) = t
    1.21 -  | type_name t (Infix _) = deprecated (strip_esc t)
    1.22 -  | type_name t (Infixl _) = deprecated (strip_esc t)
    1.23 -  | type_name t (Infixr _) = deprecated (strip_esc t)
    1.24 -  | type_name t _ = t;
    1.25 +fun type_name (InfixName _) = I
    1.26 +  | type_name (InfixlName _) = I
    1.27 +  | type_name (InfixrName _) = I
    1.28 +  | type_name (Infix _) = deprecated o strip_esc
    1.29 +  | type_name (Infixl _) = deprecated o strip_esc
    1.30 +  | type_name (Infixr _) = deprecated o strip_esc
    1.31 +  | type_name _ = I;
    1.32  
    1.33 -fun const_name c (InfixName _) = c
    1.34 -  | const_name c (InfixlName _) = c
    1.35 -  | const_name c (InfixrName _) = c
    1.36 -  | const_name c (Infix _) = "op " ^ deprecated (strip_esc c)
    1.37 -  | const_name c (Infixl _) = "op " ^ deprecated (strip_esc c)
    1.38 -  | const_name c (Infixr _) = "op " ^ deprecated (strip_esc c)
    1.39 -  | const_name c _ = c;
    1.40 +fun const_name (InfixName _) = I
    1.41 +  | const_name (InfixlName _) = I
    1.42 +  | const_name (InfixrName _) = I
    1.43 +  | const_name (Infix _) = prefix "op " o deprecated o strip_esc
    1.44 +  | const_name (Infixl _) = prefix "op " o deprecated o strip_esc
    1.45 +  | const_name (Infixr _) = prefix "op " o deprecated o strip_esc
    1.46 +  | const_name _ = I;
    1.47  
    1.48  fun fix_mixfix c (Infix p) = InfixName (c, p)
    1.49    | fix_mixfix c (Infixl p) = InfixlName (c, p)
    1.50    | fix_mixfix c (Infixr p) = InfixrName (c, p)
    1.51    | fix_mixfix _ mx = mx;
    1.52  
    1.53 -fun const_mixfix c mx = (const_name c mx, fix_mixfix c mx);
    1.54 +fun const_mixfix c mx = (const_name mx c, fix_mixfix c mx);
    1.55  
    1.56  fun map_mixfix _ NoSyn = NoSyn
    1.57    | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
    1.58 @@ -158,7 +158,7 @@
    1.59  
    1.60  fun syn_ext_types type_decls =
    1.61    let
    1.62 -    fun name_of (t, _, mx) = type_name t mx;
    1.63 +    fun name_of (t, _, mx) = type_name mx t;
    1.64  
    1.65      fun mk_infix sy t p1 p2 p3 =
    1.66        SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
    1.67 @@ -189,7 +189,7 @@
    1.68  
    1.69  fun syn_ext_consts is_logtype const_decls =
    1.70    let
    1.71 -    fun name_of (c, _, mx) = const_name c mx;
    1.72 +    fun name_of (c, _, mx) = const_name mx c;
    1.73  
    1.74      fun mk_infix sy ty c p1 p2 p3 =
    1.75        [SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),