src/Pure/Syntax/mixfix.ML
changeset 25074 78fdb4c44939
parent 22826 0f4c501a691e
child 26291 d01bf7b10c75
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Oct 17 23:16:34 2007 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Oct 17 23:16:36 2007 +0200
     1.3 @@ -31,7 +31,6 @@
     1.4    val type_name: string -> mixfix -> string
     1.5    val const_name: string -> mixfix -> string
     1.6    val const_mixfix: string -> mixfix -> string * mixfix
     1.7 -  val unlocalize_mixfix: mixfix -> mixfix
     1.8    val mixfix_args: mixfix -> int
     1.9    val mixfixT: mixfix -> typ
    1.10  end;
    1.11 @@ -140,8 +139,6 @@
    1.12    | map_mixfix _ Structure = Structure
    1.13    | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
    1.14  
    1.15 -val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
    1.16 -
    1.17  fun mixfix_args NoSyn = 0
    1.18    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
    1.19    | mixfix_args (Delimfix sy) = SynExt.mfix_args sy