src/Pure/Syntax/mixfix.ML
changeset 35390 efad0e364738
parent 35351 7425aece4ee3
child 35412 b8dead547d9e
--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 26 21:43:26 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 26 23:05:47 2010 +0100
@@ -21,7 +21,6 @@
 signature MIXFIX1 =
 sig
   include MIXFIX0
-  val literal: string -> mixfix
   val no_syn: 'a * 'b -> 'a * 'b * mixfix
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
@@ -51,8 +50,6 @@
   Binder of string * int * int |
   Structure;
 
-val literal = Delimfix o SynExt.escape_mfix;
-
 fun no_syn (x, y) = (x, y, NoSyn);