unlocalize_mixfix: fallback on NoSyn;
authorwenzelm
Tue Apr 25 22:23:50 2006 +0200 (2006-04-25)
changeset 19467d75570e8aa97
parent 19466 29bc35832a77
child 19468 0afdd5023bfc
unlocalize_mixfix: fallback on NoSyn;
src/Pure/Syntax/mixfix.ML
     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