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