src/Pure/Isar/outer_parse.ML
changeset 18618 387d170e4aa9
parent 18136 51385f358b53
child 18669 cd6d6baf0411
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Sat Jan 07 23:27:58 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Sat Jan 07 23:27:59 2006 +0100
     1.3 @@ -60,6 +60,7 @@
     1.4    val opt_mixfix': token list -> Syntax.mixfix * token list
     1.5    val mixfix': token list -> Syntax.mixfix * token list
     1.6    val const: token list -> (bstring * string * Syntax.mixfix) * token list
     1.7 +  val param: token list -> (bstring * string option * Syntax.mixfix) * token list
     1.8    val term: token list -> string * token list
     1.9    val prop: token list -> string * token list
    1.10    val propp: token list -> (string * (string list * string list)) * token list
    1.11 @@ -69,6 +70,8 @@
    1.12    val opt_attribs: token list -> Attrib.src list * token list
    1.13    val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    1.14    val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
    1.15 +  val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    1.16 +  val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    1.17    val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.18    val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.19    val xthm: token list -> (thmref * Attrib.src list) * token list
    1.20 @@ -245,8 +248,8 @@
    1.21  
    1.22  (* consts *)
    1.23  
    1.24 -val const =
    1.25 -  name -- ($$$ "::" |-- !!! (typ -- opt_mixfix)) >> triple2;
    1.26 +val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    1.27 +val param = name -- Scan.option ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    1.28  
    1.29  
    1.30  (* terms *)
    1.31 @@ -306,6 +309,9 @@
    1.32  fun opt_thm_name s =
    1.33    Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);
    1.34  
    1.35 +val spec = opt_thm_name ":" -- Scan.repeat1 prop;
    1.36 +val named_spec = thm_name ":" -- Scan.repeat1 prop;
    1.37 +
    1.38  val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.39  val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.40