src/Pure/pure_thy.ML

 
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((b, thms), atts) =
   enter_thms pre_name (name_thms false true Position.none)
-    (foldl_map (Thm.theory_attributes atts)) (b, thms);
+    (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
 
 fun gen_add_thms pre_name args =

   let
     val pos = Binding.pos_of b;
     val name = Sign.full_name thy b;
     val _ = Position.report (Markup.fact_decl name) pos;
 
-    fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
+    fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
-      (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app)
+      (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
       (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
   in ((name, thms), thy') end);
 
 in