src/Pure/Isar/attrib.ML

     fun get_named pos name = get (Facts.Named ((name, pos), NONE));
   in
     Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
       let
         val atts = map (attribute_i thy) srcs;
-        val (context', th') =
-          Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
+        val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
       in (context', pick "" [th']) end)
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
      Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>

         >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
     -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
       let
         val ths = Facts.select thmref fact;
         val atts = map (attribute_i thy) srcs;
-        val (context', ths') =
-          Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
+        val (ths', context') =
+          fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
       in (context', pick name ths') end)
   end);
 
 in