generalized (opt_)thm_name;
xthm, xthms1;

--- a/src/Pure/Isar/outer_parse.ML	Tue Nov 17 14:23:13 1998 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Tue Nov 17 14:24:15 1998 +0100
@@ -44,8 +44,10 @@
   val prop: token list -> string * token list
   val attribs: token list -> Args.src list * token list
   val opt_attribs: token list -> Args.src list * token list
-  val thm_name: token list -> (bstring * Args.src list) * token list
-  val opt_thm_name: token list -> (bstring * Args.src list) * token list
+  val thm_name: string -> token list -> (bstring * Args.src list) * token list
+  val opt_thm_name: string -> token list -> (bstring * Args.src list) * token list
+  val xthm: token list -> (xstring * Args.src list) * token list
+  val xthms1: token list -> (xstring * Args.src list) list * token list
   val method: token list -> Method.text * token list
   val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
   val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
@@ -226,8 +228,11 @@
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];
 
-val thm_name = name -- opt_attribs --| $$$ ":";
-val opt_thm_name = Scan.optional thm_name ("", []);
+fun thm_name s = name -- opt_attribs --| $$$ s;
+fun opt_thm_name s = Scan.optional (thm_name s) ("", []);
+
+val xthm = xname -- opt_attribs;
+val xthms1 = Scan.repeat1 xthm;
 
 
 (* proof methods *)