src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Tue Apr 12 14:38:57 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Apr 12 14:50:53 2016 +0200
@@ -27,6 +27,7 @@
   val reset_pos: mixfix -> mixfix
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
+  val default_constraint: mixfix -> typ
   val make_type: int -> typ
   val binder_name: string -> string
   val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
@@ -118,6 +119,12 @@
   | mixfix_args (Structure _) = 0;
 
 
+(* default type constraint *)
+
+fun default_constraint (Binder _) = (dummyT --> dummyT) --> dummyT
+  | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT;
+
+
 (* syn_ext_types *)
 
 val typeT = Type ("type", []);