src/Pure/Isar/spec_parse.ML
changeset 26336 a0e2b706ce73
parent 25999 f8bcd311d501
child 26361 7946f459c6c8
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -17,10 +17,10 @@
     1.4    val named_spec: token list -> ((bstring * Attrib.src list) * string list) * token list
     1.5    val spec_name: token list -> ((bstring * string) * Attrib.src list) * token list
     1.6    val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
     1.7 -  val xthm: token list -> (thmref * Attrib.src list) * token list
     1.8 -  val xthms1: token list -> (thmref * Attrib.src list) list * token list
     1.9 +  val xthm: token list -> (Facts.ref * Attrib.src list) * token list
    1.10 +  val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
    1.11    val name_facts: token list ->
    1.12 -    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
    1.13 +    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
    1.14    val locale_mixfix: token list -> mixfix * token list
    1.15    val locale_fixes: token list -> (string * string option * mixfix) list * token list
    1.16    val locale_insts: token list ->
    1.17 @@ -65,13 +65,13 @@
    1.18  val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    1.19  
    1.20  val thm_sel = P.$$$ "(" |-- P.list1
    1.21 - (P.nat --| P.minus -- P.nat >> PureThy.FromTo ||
    1.22 -  P.nat --| P.minus >> PureThy.From ||
    1.23 -  P.nat >> PureThy.Single) --| P.$$$ ")";
    1.24 + (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
    1.25 +  P.nat --| P.minus >> Facts.From ||
    1.26 +  P.nat >> Facts.Single) --| P.$$$ ")";
    1.27  
    1.28  val xthm =
    1.29 -  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") ||
    1.30 -  (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs;
    1.31 +  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
    1.32 +  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
    1.33  
    1.34  val xthms1 = Scan.repeat1 xthm;
    1.35