# HG changeset patch
# User wenzelm
# Date 1214659044 -7200
# Node ID 0b9295c598f6f7dcfbccc826657dfe2969376743
# Parent  ffe9b958badaed3b9cdafe81025c54a310823f9a
added thm_name, opt_thm_name;

diff -r ffe9b958bada -r 0b9295c598f6 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri Jun 27 09:55:02 2008 +0200
+++ b/src/Pure/Isar/args.ML	Sat Jun 28 15:17:24 2008 +0200
@@ -91,6 +91,8 @@
     -> ((int -> tactic) -> tactic) * ('a * T list)
   val attribs: (string -> string) -> T list -> src list * T list
   val opt_attribs: (string -> string) -> T list -> src list * T list
+  val thm_name: (string -> string) -> string -> T list -> (string * src list) * T list
+  val opt_thm_name: (string -> string) -> string -> T list -> (string * src list) * T list
   val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
   val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
     src -> Proof.context -> 'a * Proof.context
@@ -408,6 +410,13 @@
 end;
 
 
+(* theorem specifications *)
+
+fun thm_name intern s = name -- opt_attribs intern --| $$$ s;
+fun opt_thm_name intern s =
+  Scan.optional ((name -- opt_attribs intern || attribs intern >> pair "") --| $$$ s) ("", []);
+
+
 (* syntax interface *)
 
 fun syntax kind scan (src as Src ((s, args), pos)) st =