# HG changeset patch
# User wenzelm
# Date 893264984 -7200
# Node ID 588538fb9308267e06bfb8d7c40a37e7d58e31f2
# Parent  2733e21814fe21e2db4cdcb40e68444cce792600
added no_syn;

diff -r 2733e21814fe -r 588538fb9308 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Apr 22 19:08:49 1998 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Apr 22 19:09:44 1998 +0200
@@ -17,14 +17,15 @@
     Infixr of int |
     Binder of string * int * int
   val max_pri: int
-  val mixfix_args: mixfix -> int
 end;
 
 signature MIXFIX1 =
 sig
   include MIXFIX0
+  val no_syn: 'a * 'b -> 'a * 'b * mixfix
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
+  val mixfix_args: mixfix -> int
   val pure_types: (string * int * mixfix) list
   val pure_syntax: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
@@ -60,6 +61,8 @@
   Infixr of int |
   Binder of string * int * int;
 
+fun no_syn (x, y) = (x, y, NoSyn);
+
 
 (* type / const names *)