--- 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