--- a/src/Pure/Isar/outer_parse.ML Sat Jan 07 23:27:58 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML Sat Jan 07 23:27:59 2006 +0100
@@ -60,6 +60,7 @@
val opt_mixfix': token list -> Syntax.mixfix * token list
val mixfix': token list -> Syntax.mixfix * token list
val const: token list -> (bstring * string * Syntax.mixfix) * token list
+ val param: token list -> (bstring * string option * Syntax.mixfix) * token list
val term: token list -> string * token list
val prop: token list -> string * token list
val propp: token list -> (string * (string list * string list)) * token list
@@ -69,6 +70,8 @@
val opt_attribs: token list -> Attrib.src list * token list
val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
+ val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
+ val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
val xthm: token list -> (thmref * Attrib.src list) * token list
@@ -245,8 +248,8 @@
(* consts *)
-val const =
- name -- ($$$ "::" |-- !!! (typ -- opt_mixfix)) >> triple2;
+val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val param = name -- Scan.option ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
(* terms *)
@@ -306,6 +309,9 @@
fun opt_thm_name s =
Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);
+val spec = opt_thm_name ":" -- Scan.repeat1 prop;
+val named_spec = thm_name ":" -- Scan.repeat1 prop;
+
val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));