Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Syntax/mixfix.ML
changeset 19467 d75570e8aa97
parent 19373 f2446ce04590
child 19482 9f11af8f7ef9 
--- 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
isabelle