1.1 --- a/NEWS	Wed Feb 24 07:06:39 2010 -0800
     1.2 +++ b/NEWS	Wed Feb 24 20:37:01 2010 +0100
     1.3 @@ -38,6 +38,8 @@
     1.4  and ML_command "set Syntax.trace_ast" help to diagnose syntax
     1.5  problems.
     1.6  
     1.7 +* Type constructors admit general mixfix syntax, not just infix.
     1.8 +
     1.9  
    1.10  *** Pure ***
    1.11  

     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 24 07:06:39 2010 -0800
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 24 20:37:01 2010 +0100
     2.3 @@ -13,14 +13,14 @@
     2.4    \end{matharray}
     2.5  
     2.6    \begin{rail}
     2.7 -    'typedecl' typespec infix?
     2.8 +    'typedecl' typespec mixfix?
     2.9      ;
    2.10      'typedef' altname? abstype '=' repset
    2.11      ;
    2.12  
    2.13      altname: '(' (name | 'open' | 'open' name) ')'
    2.14      ;
    2.15 -    abstype: typespec infix?
    2.16 +    abstype: typespec mixfix?
    2.17      ;
    2.18      repset: term ('morphisms' name name)?
    2.19      ;
    2.20 @@ -367,7 +367,7 @@
    2.21      'rep\_datatype' ('(' (name +) ')')? (term +)
    2.22      ;
    2.23  
    2.24 -    dtspec: parname? typespec infix? '=' (cons + '|')
    2.25 +    dtspec: parname? typespec mixfix? '=' (cons + '|')
    2.26      ;
    2.27      cons: name ( type * ) mixfix?
    2.28    \end{rail}

     3.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Feb 24 07:06:39 2010 -0800
     3.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Feb 24 20:37:01 2010 +0100
     3.3 @@ -244,11 +244,9 @@
     3.4  section {* Mixfix annotations *}
     3.5  
     3.6  text {* Mixfix annotations specify concrete \emph{inner syntax} of
     3.7 -  Isabelle types and terms.  Some commands such as @{command
     3.8 -  "typedecl"} admit infixes only, while @{command "definition"} etc.\
     3.9 -  support the full range of general mixfixes and binders.  Fixed
    3.10 -  parameters in toplevel theorem statements, locale specifications
    3.11 -  also admit mixfix annotations.
    3.12 +  Isabelle types and terms.  Locally fixed parameters in toplevel
    3.13 +  theorem statements, locale specifications etc.\ also admit mixfix
    3.14 +  annotations.
    3.15  
    3.16    \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
    3.17    \begin{rail}

     4.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Feb 24 07:06:39 2010 -0800
     4.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Feb 24 20:37:01 2010 +0100
     4.3 @@ -959,9 +959,9 @@
     4.4    \end{matharray}
     4.5  
     4.6    \begin{rail}
     4.7 -    'types' (typespec '=' type infix? +)
     4.8 +    'types' (typespec '=' type mixfix? +)
     4.9      ;
    4.10 -    'typedecl' typespec infix?
    4.11 +    'typedecl' typespec mixfix?
    4.12      ;
    4.13      'arities' (nameref '::' arity +)
    4.14      ;

     5.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 24 07:06:39 2010 -0800
     5.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 24 20:37:01 2010 +0100
     5.3 @@ -33,14 +33,14 @@
     5.4    \end{matharray}
     5.5  
     5.6    \begin{rail}
     5.7 -    'typedecl' typespec infix?
     5.8 +    'typedecl' typespec mixfix?
     5.9      ;
    5.10      'typedef' altname? abstype '=' repset
    5.11      ;
    5.12  
    5.13      altname: '(' (name | 'open' | 'open' name) ')'
    5.14      ;
    5.15 -    abstype: typespec infix?
    5.16 +    abstype: typespec mixfix?
    5.17      ;
    5.18      repset: term ('morphisms' name name)?
    5.19      ;
    5.20 @@ -372,7 +372,7 @@
    5.21      'rep\_datatype' ('(' (name +) ')')? (term +)
    5.22      ;
    5.23  
    5.24 -    dtspec: parname? typespec infix? '=' (cons + '|')
    5.25 +    dtspec: parname? typespec mixfix? '=' (cons + '|')
    5.26      ;
    5.27      cons: name ( type * ) mixfix?
    5.28    \end{rail}
    5.29 @@ -906,6 +906,9 @@
    5.30        \item[iterations] sets how many sets of assignments are
    5.31          generated for each particular size.
    5.32  
    5.33 +      \item[no\_assms] specifies whether assumptions in
    5.34 +        structured proofs should be ignored.
    5.35 +
    5.36      \end{description}
    5.37  
    5.38      These option can be given within square brackets.

     6.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 07:06:39 2010 -0800
     6.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Feb 24 20:37:01 2010 +0100
     6.3 @@ -266,10 +266,9 @@
     6.4  %
     6.5  \begin{isamarkuptext}%
     6.6  Mixfix annotations specify concrete \emph{inner syntax} of
     6.7 -  Isabelle types and terms.  Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\
     6.8 -  support the full range of general mixfixes and binders.  Fixed
     6.9 -  parameters in toplevel theorem statements, locale specifications
    6.10 -  also admit mixfix annotations.
    6.11 +  Isabelle types and terms.  Locally fixed parameters in toplevel
    6.12 +  theorem statements, locale specifications etc.\ also admit mixfix
    6.13 +  annotations.
    6.14  
    6.15    \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
    6.16    \begin{rail}

     7.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Feb 24 07:06:39 2010 -0800
     7.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Feb 24 20:37:01 2010 +0100
     7.3 @@ -996,9 +996,9 @@
     7.4    \end{matharray}
     7.5  
     7.6    \begin{rail}
     7.7 -    'types' (typespec '=' type infix? +)
     7.8 +    'types' (typespec '=' type mixfix? +)
     7.9      ;
    7.10 -    'typedecl' typespec infix?
    7.11 +    'typedecl' typespec mixfix?
    7.12      ;
    7.13      'arities' (nameref '::' arity +)
    7.14      ;

     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Feb 24 07:06:39 2010 -0800
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Feb 24 20:37:01 2010 +0100
     8.3 @@ -2079,7 +2079,7 @@
     8.4  local structure P = OuterParse and K = OuterKeyword in
     8.5  
     8.6  val datatype_decl =
     8.7 -  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
     8.8 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
     8.9      (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
    8.10  
    8.11  fun mk_datatype args =

     9.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Feb 24 07:06:39 2010 -0800
     9.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Feb 24 20:37:01 2010 +0100
     9.3 @@ -731,7 +731,7 @@
     9.4    in (names, specs) end;
     9.5  
     9.6  val parse_datatype_decl =
     9.7 -  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
     9.8 +  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
     9.9      (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
    9.10  
    9.11  val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;

    10.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Feb 24 07:06:39 2010 -0800
    10.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Feb 24 20:37:01 2010 +0100
    10.3 @@ -296,7 +296,7 @@
    10.4  val quotspec_parser =
    10.5      OuterParse.and_list1
    10.6       ((OuterParse.type_args -- OuterParse.binding) --
    10.7 -        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
    10.8 +        OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
    10.9           (OuterParse.$$$ "/" |-- OuterParse.term))
   10.10  
   10.11  val _ = OuterKeyword.keyword "/"

    11.1 --- a/src/HOL/Tools/typedef.ML	Wed Feb 24 07:06:39 2010 -0800
    11.2 +++ b/src/HOL/Tools/typedef.ML	Wed Feb 24 20:37:01 2010 +0100
    11.3 @@ -255,7 +255,7 @@
    11.4      (Scan.optional (P.$$$ "(" |--
    11.5          ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
    11.6            P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
    11.7 -      (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    11.8 +      (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    11.9        Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
   11.10      >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
   11.11          Toplevel.print o Toplevel.theory_to_proof

    12.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Feb 24 07:06:39 2010 -0800
    12.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Feb 24 20:37:01 2010 +0100
    12.3 @@ -291,7 +291,7 @@
    12.4    || Scan.succeed [];
    12.5  
    12.6  val domain_decl =
    12.7 -  (type_args' -- P.binding -- P.opt_infix) --
    12.8 +  (type_args' -- P.binding -- P.opt_mixfix) --
    12.9      (P.$$$ "=" |-- P.enum1 "|" cons_decl);
   12.10  
   12.11  val domains_decl =

    13.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Feb 24 07:06:39 2010 -0800
    13.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Feb 24 20:37:01 2010 +0100
    13.3 @@ -700,7 +700,7 @@
    13.4  val parse_domain_iso :
    13.5      (string list * binding * mixfix * string * (binding * binding) option)
    13.6        parser =
    13.7 -  (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ) --
    13.8 +  (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
    13.9      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
   13.10      >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
   13.11  

    14.1 --- a/src/HOLCF/Tools/pcpodef.ML	Wed Feb 24 07:06:39 2010 -0800
    14.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Wed Feb 24 20:37:01 2010 +0100
    14.3 @@ -340,7 +340,7 @@
    14.4    Scan.optional (P.$$$ "(" |--
    14.5        ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
    14.6          --| P.$$$ ")") (true, NONE) --
    14.7 -    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    14.8 +    (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    14.9      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   14.10  
   14.11  fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =

    15.1 --- a/src/HOLCF/Tools/repdef.ML	Wed Feb 24 07:06:39 2010 -0800
    15.2 +++ b/src/HOLCF/Tools/repdef.ML	Wed Feb 24 20:37:01 2010 +0100
    15.3 @@ -167,7 +167,7 @@
    15.4    Scan.optional (P.$$$ "(" |--
    15.5        ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
    15.6          --| P.$$$ ")") (true, NONE) --
    15.7 -    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    15.8 +    (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    15.9      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   15.10  
   15.11  fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =

    16.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Feb 24 07:06:39 2010 -0800
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 24 20:37:01 2010 +0100
    16.3 @@ -104,13 +104,13 @@
    16.4  
    16.5  val _ =
    16.6    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
    16.7 -    (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) =>
    16.8 +    (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
    16.9        Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
   16.10  
   16.11  val _ =
   16.12    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   16.13      (Scan.repeat1
   16.14 -      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
   16.15 +      (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
   16.16        >> (Toplevel.theory o Sign.add_tyabbrs o
   16.17          map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   16.18  

    17.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Feb 24 07:06:39 2010 -0800
    17.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Feb 24 20:37:01 2010 +0100
    17.3 @@ -72,8 +72,6 @@
    17.4    val typ: string parser
    17.5    val mixfix: mixfix parser
    17.6    val mixfix': mixfix parser
    17.7 -  val opt_infix: mixfix parser
    17.8 -  val opt_infix': mixfix parser
    17.9    val opt_mixfix: mixfix parser
   17.10    val opt_mixfix': mixfix parser
   17.11    val where_: string parser
   17.12 @@ -279,8 +277,6 @@
   17.13  
   17.14  val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
   17.15  val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
   17.16 -val opt_infix = opt_annotation !!! (infxl || infxr || infx);
   17.17 -val opt_infix' = opt_annotation I (infxl || infxr || infx);
   17.18  val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
   17.19  val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
   17.20  

    18.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Feb 24 07:06:39 2010 -0800
    18.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Feb 24 20:37:01 2010 +0100
    18.3 @@ -101,20 +101,26 @@
    18.4  
    18.5  fun syn_ext_types type_decls =
    18.6    let
    18.7 -    fun mk_infix sy t p1 p2 p3 =
    18.8 -      SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
    18.9 -        [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3);
   18.10 +    fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT;
   18.11 +    fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3);
   18.12  
   18.13      fun mfix_of (_, _, NoSyn) = NONE
   18.14 -      | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p)
   18.15 -      | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p)
   18.16 -      | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p)
   18.17 -      | mfix_of (t, _, _) =
   18.18 -          error ("Bad mixfix declaration for type: " ^ quote t);  (* FIXME printable!? *)
   18.19 +      | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p))
   18.20 +      | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri))
   18.21 +      | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p)
   18.22 +      | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p)
   18.23 +      | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p)
   18.24 +      | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
   18.25  
   18.26 -    val mfix = map_filter mfix_of type_decls;
   18.27 +    fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
   18.28 +          if SynExt.mfix_args sy = n then ()
   18.29 +          else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
   18.30 +      | check_args _ NONE = ();
   18.31 +
   18.32 +    val mfix = map mfix_of type_decls;
   18.33 +    val _ = map2 check_args type_decls mfix;
   18.34      val xconsts = map #1 type_decls;
   18.35 -  in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
   18.36 +  in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
   18.37  
   18.38  
   18.39  (* syn_ext_consts *)
   18.40 @@ -140,7 +146,7 @@
   18.41        | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
   18.42        | mfix_of (c, ty, Binder (sy, p, q)) =
   18.43            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
   18.44 -      | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c);
   18.45 +      | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);   (* FIXME printable c (!?) *)
   18.46  
   18.47      fun binder (c, _, Binder _) = SOME (binder_name c, c)
   18.48        | binder _ = NONE;

    19.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Feb 24 07:06:39 2010 -0800
    19.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Feb 24 20:37:01 2010 +0100
    19.3 @@ -28,6 +28,8 @@
    19.4    val cargs: string
    19.5    val any: string
    19.6    val sprop: string
    19.7 +  datatype mfix = Mfix of string * typ * string * int list * int
    19.8 +  val err_in_mfix: string -> mfix -> 'a
    19.9    val typ_to_nonterm: typ -> string
   19.10    datatype xsymb =
   19.11      Delim of string |
   19.12 @@ -37,7 +39,6 @@
   19.13    datatype xprod = XProd of string * xsymb list * string * int
   19.14    val chain_pri: int
   19.15    val delims_of: xprod list -> string list list
   19.16 -  datatype mfix = Mfix of string * typ * string * int list * int
   19.17    datatype syn_ext =
   19.18      SynExt of {
   19.19        xprods: xprod list,