src/Pure/Syntax/syn_ext.ML
changeset 35352 7425aece4ee3
parent 35113 dc4f61a7918a
child 35390 efad0e364738
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Feb 24 07:06:39 2010 -0800
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Feb 24 20:37:01 2010 +0100
     1.3 @@ -28,6 +28,8 @@
     1.4    val cargs: string
     1.5    val any: string
     1.6    val sprop: string
     1.7 +  datatype mfix = Mfix of string * typ * string * int list * int
     1.8 +  val err_in_mfix: string -> mfix -> 'a
     1.9    val typ_to_nonterm: typ -> string
    1.10    datatype xsymb =
    1.11      Delim of string |
    1.12 @@ -37,7 +39,6 @@
    1.13    datatype xprod = XProd of string * xsymb list * string * int
    1.14    val chain_pri: int
    1.15    val delims_of: xprod list -> string list list
    1.16 -  datatype mfix = Mfix of string * typ * string * int list * int
    1.17    datatype syn_ext =
    1.18      SynExt of {
    1.19        xprods: xprod list,