# HG changeset patch
# User wenzelm
# Date 1012395636 -3600
# Node ID cecaa6e64fd5c692741445c5c7413b8d02ac824f
# Parent  cc4dd256564fa01eb0f29d4a76a1347381b89aee
added literal;

diff -r cc4dd256564f -r cecaa6e64fd5 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);