--- a/src/Pure/General/buffer.ML Sun Jun 03 23:16:53 2007 +0200
+++ b/src/Pure/General/buffer.ML Sun Jun 03 23:16:54 2007 +0200
@@ -29,6 +29,6 @@
fun write path (Buffer xs) = File.write_list path (rev xs);
-fun output f (Buffer xs) = Library.seq f (rev xs);
+fun output f (Buffer xs) = List.app f (rev xs);
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Jun 03 23:16:53 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Jun 03 23:16:54 2007 +0200
@@ -625,7 +625,7 @@
| (NONE, SOME ObjTheorem) =>
(* A large query, but not unreasonable. ~5000 results for HOL.*)
(* Several setids should be allowed, but Eclipse code is currently broken:
- Library.seq (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
+ List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
(ThyInfo.names()) *)
setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
(maps qualified_thms_of_thy (ThyInfo.names())))
--- a/src/Pure/Tools/nbe.ML Sun Jun 03 23:16:53 2007 +0200
+++ b/src/Pure/Tools/nbe.ML Sun Jun 03 23:16:54 2007 +0200
@@ -103,7 +103,7 @@
(!trace) s);
val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs) ();
val _ = tab := NBE_Data.get thy;;
- val _ = Library.seq (use_code o NBE_Codegen.generate thy
+ val _ = List.app (use_code o NBE_Codegen.generate thy
(fn s => Symtab.defined (!tab) s)) funs;
in NBE_Data.change thy (K (!tab)) end;