1.1 --- a/src/Pure/Isar/args.ML	Tue Sep 02 14:10:27 2008 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Sep 02 14:10:28 2008 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    val name_source: T list -> string * T list
     1.5    val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
     1.6    val name: T list -> string * T list
     1.7 +  val binding: T list -> Name.binding * T list
     1.8    val alt_name: T list -> string * T list
     1.9    val symbol: T list -> string * T list
    1.10    val liberal_name: T list -> string * T list
    1.11 @@ -65,8 +66,8 @@
    1.12    val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
    1.13    val attribs: (string -> string) -> T list -> src list * T list
    1.14    val opt_attribs: (string -> string) -> T list -> src list * T list
    1.15 -  val thm_name: (string -> string) -> string -> T list -> (string * src list) * T list
    1.16 -  val opt_thm_name: (string -> string) -> string -> T list -> (string * src list) * T list
    1.17 +  val thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
    1.18 +  val opt_thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
    1.19    val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
    1.20    val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
    1.21      src -> Proof.context -> 'a * Proof.context
    1.22 @@ -170,6 +171,7 @@
    1.23  val name_source_position = named >> T.source_position_of;
    1.24  
    1.25  val name = named >> T.content_of;
    1.26 +val binding = P.position name >> Name.binding_pos;
    1.27  val alt_name = alt_string >> T.content_of;
    1.28  val symbol = symbolic >> T.content_of;
    1.29  val liberal_name = symbol || name;
    1.30 @@ -274,10 +276,12 @@
    1.31  
    1.32  (* theorem specifications *)
    1.33  
    1.34 -fun thm_name intern s = name -- opt_attribs intern --| $$$ s;
    1.35 +fun thm_name intern s = binding -- opt_attribs intern --| $$$ s;
    1.36  
    1.37  fun opt_thm_name intern s =
    1.38 -  Scan.optional ((name -- opt_attribs intern || attribs intern >> pair "") --| $$$ s) ("", []);
    1.39 +  Scan.optional
    1.40 +    ((binding -- opt_attribs intern || attribs intern >> pair Name.no_binding) --| $$$ s)
    1.41 +    (Name.no_binding, []);
    1.42  
    1.43  
    1.44