removed obsolete Library.seq;
authorwenzelm
Sun, 03 Jun 2007 23:16:54 +0200
changeset 23226 441f8a0bd766
parent 23225 591af6a2f09e
child 23227 96f86d377dd9
removed obsolete Library.seq;
src/Pure/General/buffer.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Tools/nbe.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;
--- 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;