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 21805 6af1aa7f67d6
parent 21534 68f805e9db0b
child 22702 372da033ed93 
--- a/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:31 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Dec 12 20:49:32 2006 +0100
@@ -31,7 +31,7 @@
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val const_mixfix: string -> mixfix -> string * mixfix
-  val unlocalize_mixfix: bool -> mixfix -> mixfix
+  val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
 end;
 
@@ -139,9 +139,7 @@
   | map_mixfix _ Structure = Structure
   | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
 
-fun unlocalize_mixfix loc mx =
-  let val mx' = map_mixfix SynExt.unlocalize_mfix mx
-  in if mx = mx' andalso loc then NoSyn else mx' end;
+val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
 
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
isabelle