# HG changeset patch
# User wenzelm
# Date 1180905414 -7200
# Node ID 441f8a0bd766c54258ba3354fa590a4f4a1f2e15
# Parent  591af6a2f09e4cd993b2981a22739ce351408397
removed obsolete Library.seq;

diff -r 591af6a2f09e -r 441f8a0bd766 src/Pure/General/buffer.ML
--- 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;
diff -r 591af6a2f09e -r 441f8a0bd766 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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())))
diff -r 591af6a2f09e -r 441f8a0bd766 src/Pure/Tools/nbe.ML
--- 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;