diff -r 2b8ac8bc9719 -r 818a24371de9 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Jan 04 00:52:47 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jan 04 00:52:48 2006 +0100
@@ -14,9 +14,9 @@
     InfixName of string * int |
     InfixlName of string * int |
     InfixrName of string * int |
-    Infix of int |
-    Infixl of int |
-    Infixr of int |
+    Infix of int |    (*obsolete*)
+    Infixl of int |   (*obsolete*)
+    Infixr of int |   (*obsolete*)
     Binder of string * int * int
 end;
 
@@ -29,6 +29,7 @@
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val fix_mixfix: string -> mixfix -> mixfix
+  val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
   val pure_nonterms: string list
   val pure_syntax: (string * string * mixfix) list
@@ -58,9 +59,9 @@
   InfixName of string * int |
   InfixlName of string * int |
   InfixrName of string * int |
-  Infix of int |
-  Infixl of int |
-  Infixr of int |
+  Infix of int |      (*obsolete*)
+  Infixl of int |     (*obsolete*)
+  Infixr of int |     (*obsolete*)
   Binder of string * int * int;
 
 val literal = Delimfix o SynExt.escape_mfix;
@@ -120,6 +121,17 @@
   | fix_mixfix c (Infixr p) = (deprecated (strip_esc c); InfixrName (c, p))
   | fix_mixfix _ mx = mx;
 
+fun map_mixfix _ NoSyn = NoSyn
+  | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
+  | map_mixfix f (Delimfix sy) = Delimfix (f sy)
+  | map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p)
+  | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
+  | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
+  | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
+  | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
+
+val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
+
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
   | mixfix_args (Delimfix sy) = SynExt.mfix_args sy