src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Wed Jan 30 14:00:25 2002 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jan 30 14:00:36 2002 +0100
@@ -24,6 +24,7 @@
 signature MIXFIX1 =
 sig
   include MIXFIX0
+  val literal: string -> mixfix
   val no_syn: 'a * 'b -> 'a * 'b * mixfix
   val string_of_mixfix: mixfix -> string
   val type_name: string -> mixfix -> string
@@ -66,6 +67,8 @@
   Infixr of int |
   Binder of string * int * int;
 
+val literal = Delimfix o SynExt.escape_mfix;
+
 fun no_syn (x, y) = (x, y, NoSyn);