# HG changeset patch # User wenzelm # Date 1145996630 -7200 # Node ID d75570e8aa976e417540f9dd500a21246401c3ce # Parent 29bc35832a779a341fecfad53aa1b2a467f47f63 unlocalize_mixfix: fallback on NoSyn; diff -r 29bc35832a77 -r d75570e8aa97 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Apr 25 22:23:41 2006 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Apr 25 22:23:50 2006 +0200 @@ -143,7 +143,9 @@ | map_mixfix _ Structure = Structure | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix"); -val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix; +fun unlocalize_mixfix mx = + let val mx' = map_mixfix SynExt.unlocalize_mfix mx + in if mx = mx' then NoSyn else mx' end; fun mixfix_args NoSyn = 0 | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy