src/Pure/Syntax/mixfix.ML
changeset 19467 d75570e8aa97
parent 19373 f2446ce04590
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Apr 25 22:23:41 2006 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Apr 25 22:23:50 2006 +0200
     1.3 @@ -143,7 +143,9 @@
     1.4    | map_mixfix _ Structure = Structure
     1.5    | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
     1.6  
     1.7 -val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
     1.8 +fun unlocalize_mixfix mx =
     1.9 +  let val mx' = map_mixfix SynExt.unlocalize_mfix mx
    1.10 +  in if mx = mx' then NoSyn else mx' end;
    1.11  
    1.12  fun mixfix_args NoSyn = 0
    1.13    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy