src/Pure/Isar/attrib.ML
changeset 26361 7946f459c6c8
parent 26345 f70620a4cf81
child 26435 bdce320cd426
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Mar 20 12:09:22 2008 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Mar 20 16:04:30 2008 +0100
     1.3 @@ -163,8 +163,8 @@
     1.4    let
     1.5      val thy = Context.theory_of context;
     1.6      val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
     1.7 -    fun get_fact s = get (Facts.Fact s);
     1.8 -    fun get_named s = get (Facts.Named (s, NONE));
     1.9 +    val get_fact = get o Facts.Fact;
    1.10 +    val get_named = get o Facts.named;
    1.11    in
    1.12      Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
    1.13        let
    1.14 @@ -174,8 +174,8 @@
    1.15      ||
    1.16      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.17        >> (fn (s, fact) => ("", Facts.Fact s, fact))
    1.18 -    || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
    1.19 -      >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
    1.20 +    || Scan.ahead fact_name -- Args.position (Args.named_fact get_named) -- Scan.option Args.thm_sel
    1.21 +      >> (fn ((name, (fact, pos)), sel) => (name, Facts.Named ((name, pos), sel), fact)))
    1.22      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    1.23        let
    1.24          val ths = Facts.select thmref fact;