# HG changeset patch
# User wenzelm
# Date 1136672879 -3600
# Node ID 387d170e4aa91cb1ed72df5bff428ccb35a28cf8
# Parent  8928e8722301d2464d4df7bad5d96541840ae62f
added param, spec, named_spec;

diff -r 8928e8722301 -r 387d170e4aa9 src/Pure/Isar/outer_parse.ML
--- 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));