src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Mon Mar 01 09:47:44 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Mon Mar 01 17:07:36 2010 +0100
@@ -25,12 +25,13 @@
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
   val mixfixT: mixfix -> typ
+  val make_type: int -> typ
 end;
 
 signature MIXFIX =
 sig
   include MIXFIX1
-  val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
+  val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
   val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
 end;
 
@@ -96,21 +97,22 @@
 
 (* syn_ext_types *)
 
+fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
+
 fun syn_ext_types type_decls =
   let
-    fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
-    fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
+    fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
 
     fun mfix_of (_, _, NoSyn) = NONE
-      | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
-      | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
-      | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
-      | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
-      | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
+      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
+      | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
+      | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
+      | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
+      | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
       | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
 
-    fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
-          if SynExt.mfix_args sy = n then ()
+    fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
+          if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
           else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
       | check_args _ NONE = ();