src/Pure/Syntax/mixfix.ML
changeset 21805 6af1aa7f67d6
parent 21534 68f805e9db0b
child 22702 372da033ed93
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:31 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:32 2006 +0100
     1.3 @@ -31,7 +31,7 @@
     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: bool -> mixfix -> mixfix
     1.8 +  val unlocalize_mixfix: mixfix -> mixfix
     1.9    val mixfix_args: mixfix -> int
    1.10  end;
    1.11  
    1.12 @@ -139,9 +139,7 @@
    1.13    | map_mixfix _ Structure = Structure
    1.14    | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
    1.15  
    1.16 -fun unlocalize_mixfix loc mx =
    1.17 -  let val mx' = map_mixfix SynExt.unlocalize_mfix mx
    1.18 -  in if mx = mx' andalso loc then NoSyn else mx' end;
    1.19 +val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
    1.20  
    1.21  fun mixfix_args NoSyn = 0
    1.22    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy