src/Pure/Isar/spec_parse.ML
changeset 28083 103d9282a946
parent 27816 0dfed2f2822a
child 28084 a05ca48ef263
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Tue Sep 02 14:10:45 2008 +0200
     1.3 @@ -11,34 +11,34 @@
     1.4    val attrib: OuterLex.token list -> Attrib.src * token list
     1.5    val attribs: token list -> Attrib.src list * token list
     1.6    val opt_attribs: token list -> Attrib.src list * token list
     1.7 -  val thm_name: string -> token list -> (bstring * Attrib.src list) * token list
     1.8 -  val opt_thm_name: string -> token list -> (bstring * Attrib.src list) * token list
     1.9 -  val spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    1.10 -  val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
    1.11 -  val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.12 -  val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
    1.13 +  val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
    1.14 +  val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
    1.15 +  val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
    1.16 +  val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
    1.17 +  val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
    1.18 +  val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
    1.19    val xthm: token list -> (Facts.ref * Attrib.src list) * token list
    1.20    val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
    1.21    val name_facts: token list ->
    1.22 -    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
    1.23 +    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
    1.24    val locale_mixfix: token list -> mixfix * token list
    1.25 -  val locale_fixes: token list -> (string * string option * mixfix) list * token list
    1.26 +  val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
    1.27    val locale_insts: token list ->
    1.28 -    (string option list * ((bstring * Attrib.src list) * string) list) * token list
    1.29 +    (string option list * ((Name.binding * Attrib.src list) * string) list) * token list
    1.30    val class_expr: token list -> string list * token list
    1.31    val locale_expr: token list -> Locale.expr * token list
    1.32    val locale_keyword: token list -> string * token list
    1.33    val locale_element: token list -> Element.context Locale.element * token list
    1.34    val context_element: token list -> Element.context * token list
    1.35    val statement: token list ->
    1.36 -    ((bstring * Attrib.src list) * (string * string list) list) list * token list
    1.37 +    ((Name.binding * Attrib.src list) * (string * string list) list) list * token list
    1.38    val general_statement: token list ->
    1.39      (Element.context Locale.element list * Element.statement) * OuterLex.token list
    1.40    val statement_keyword: token list -> string * token list
    1.41    val specification: token list ->
    1.42 -    (string *
    1.43 -      (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
    1.44 -    token list
    1.45 +    (Name.binding *
    1.46 +      (((Name.binding * Attrib.src list) * string list) list *
    1.47 +        (Name.binding * string option) list)) list * token list
    1.48  end;
    1.49  
    1.50  structure SpecParse: SPEC_PARSE =
    1.51 @@ -54,9 +54,11 @@
    1.52  val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
    1.53  val opt_attribs = Scan.optional attribs [];
    1.54  
    1.55 -fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
    1.56 +fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
    1.57 +
    1.58  fun opt_thm_name s =
    1.59 -  Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []);
    1.60 +  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
    1.61 +    (Name.no_binding, []);
    1.62  
    1.63  val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
    1.64  val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    1.65 @@ -79,7 +81,7 @@
    1.66  val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
    1.67  
    1.68  val locale_fixes =
    1.69 -  P.and_list1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
    1.70 +  P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
    1.71      >> (single o P.triple1) ||
    1.72    P.params >> map Syntax.no_syn) >> flat;
    1.73  
    1.74 @@ -134,7 +136,7 @@
    1.75  val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
    1.76  
    1.77  val obtain_case =
    1.78 -  P.parname -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
    1.79 +  P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] --
    1.80      (P.and_list1 (Scan.repeat1 P.prop) >> flat));
    1.81  
    1.82  val general_statement =
    1.83 @@ -148,6 +150,6 @@
    1.84  
    1.85  (* specifications *)
    1.86  
    1.87 -val specification = P.enum1 "|" (P.parname -- (P.and_list1 spec -- P.for_simple_fixes));
    1.88 +val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes));
    1.89  
    1.90  end;