src/Pure/Isar/attrib.ML
changeset 27820 56515e560104
parent 27812 af8edf3ab68c
child 27865 27a8ad9612a3
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Aug 10 12:38:23 2008 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Aug 10 12:38:24 2008 +0200
     1.3 @@ -172,18 +172,19 @@
     1.4      val thy = Context.theory_of context;
     1.5      val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
     1.6      val get_fact = get o Facts.Fact;
     1.7 -    val get_named = get o Facts.named;
     1.8 +    fun get_named pos name = get (Facts.Named ((name, pos), NONE));
     1.9    in
    1.10 -    Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
    1.11 +    P.$$$ "[" |-- Args.attribs (intern thy) --| P.$$$ "]" >> (fn srcs =>
    1.12        let
    1.13          val atts = map (attribute_i thy) srcs;
    1.14          val (context', th') = Library.apply atts (context, Drule.dummy_thm);
    1.15        in (context', pick "" [th']) end)
    1.16      ||
    1.17      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.18 -      >> (fn (s, fact) => ("", Facts.Fact s, fact))
    1.19 -    || Scan.ahead fact_name -- P.position (Args.named_fact get_named) -- Scan.option thm_sel
    1.20 -      >> (fn ((name, (fact, pos)), sel) => (name, Facts.Named ((name, pos), sel), fact)))
    1.21 +      >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    1.22 +     Scan.ahead (P.position fact_name) :|-- (fn (name, pos) =>
    1.23 +      Args.named_fact (get_named pos) -- Scan.option thm_sel
    1.24 +        >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
    1.25      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    1.26        let
    1.27          val ths = Facts.select thmref fact;
    1.28 @@ -344,7 +345,7 @@
    1.29  
    1.30  local
    1.31  
    1.32 -val equals = Args.$$$ "=";
    1.33 +val equals = P.$$$ "=";
    1.34  
    1.35  fun scan_value (Config.Bool _) =
    1.36        equals -- Args.$$$ "false" >> K (Config.Bool false) ||