src/Pure/Isar/attrib.ML
changeset 46775 6287653e63ec
parent 46512 4f9f61f9b535
child 46903 3d44892ac0d6
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Mar 03 18:18:39 2012 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Mar 03 21:43:59 2012 +0100
     1.3 @@ -191,8 +191,7 @@
     1.4      Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
     1.5        let
     1.6          val atts = map (attribute_i thy) srcs;
     1.7 -        val (context', th') =
     1.8 -          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
     1.9 +        val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
    1.10        in (context', pick "" [th']) end)
    1.11      ||
    1.12      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.13 @@ -204,8 +203,8 @@
    1.14        let
    1.15          val ths = Facts.select thmref fact;
    1.16          val atts = map (attribute_i thy) srcs;
    1.17 -        val (context', ths') =
    1.18 -          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
    1.19 +        val (ths', context') =
    1.20 +          fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
    1.21        in (context', pick name ths') end)
    1.22    end);
    1.23