# HG changeset patch
# User wenzelm
# Date 1192655796 -7200
# Node ID 78fdb4c449398aaf92d34d4a521371dbbcaf7868
# Parent  13db30d367d299d61fa7495a4f6e6ec9d8bf60b9
removed obsolete unlocalize_mixfix;

diff -r 13db30d367d2 -r 78fdb4c44939 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Oct 17 23:16:34 2007 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Oct 17 23:16:36 2007 +0200
@@ -31,7 +31,6 @@
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val const_mixfix: string -> mixfix -> string * mixfix
-  val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
   val mixfixT: mixfix -> typ
 end;
@@ -140,8 +139,6 @@
   | map_mixfix _ Structure = Structure
   | 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