# HG changeset patch
# User wenzelm
# Date 1220357428 -7200
# Node ID 0c420e7579a68e6e8d8e609cb1351d5fb61c7603
# Parent  d6102a4fcfce8d6cd95dec33720699c2809985c4
added binding;
thm_name/opt_thm_name: Name.binding;

diff -r d6102a4fcfce -r 0c420e7579a6 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Sep 02 14:10:27 2008 +0200
+++ b/src/Pure/Isar/args.ML	Tue Sep 02 14:10:28 2008 +0200
@@ -35,6 +35,7 @@
   val name_source: T list -> string * T list
   val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
   val name: T list -> string * T list
+  val binding: T list -> Name.binding * T list
   val alt_name: T list -> string * T list
   val symbol: T list -> string * T list
   val liberal_name: T list -> string * T list
@@ -65,8 +66,8 @@
   val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token 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 thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
+  val opt_thm_name: (string -> string) -> string -> T list -> (Name.binding * 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
@@ -170,6 +171,7 @@
 val name_source_position = named >> T.source_position_of;
 
 val name = named >> T.content_of;
+val binding = P.position name >> Name.binding_pos;
 val alt_name = alt_string >> T.content_of;
 val symbol = symbolic >> T.content_of;
 val liberal_name = symbol || name;
@@ -274,10 +276,12 @@
 
 (* theorem specifications *)
 
-fun thm_name intern s = name -- opt_attribs intern --| $$$ s;
+fun thm_name intern s = binding -- opt_attribs intern --| $$$ s;
 
 fun opt_thm_name intern s =
-  Scan.optional ((name -- opt_attribs intern || attribs intern >> pair "") --| $$$ s) ("", []);
+  Scan.optional
+    ((binding -- opt_attribs intern || attribs intern >> pair Name.no_binding) --| $$$ s)
+    (Name.no_binding, []);