added no_syn;
authorwenzelm
Wed, 22 Apr 1998 19:09:44 +0200
changeset 4823 588538fb9308
parent 4822 2733e21814fe
child 4824 df8fc4626a9e
added no_syn;
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 *)