put "foldl" and "foldr" in "Useful";
Isabelle hides those symbols from List, but by adding them to Useful we have them throughout Metis without "List." prefix
--- a/src/Tools/Metis/src/Useful.sig Wed Sep 15 15:15:49 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sig Wed Sep 15 15:44:24 2010 +0200
@@ -107,6 +107,10 @@
(* Lists: note we count elements from 0. *)
(* ------------------------------------------------------------------------- *)
+val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
+
+val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
+
val cons : 'a -> 'a list -> 'a list
val hdTl : 'a list -> 'a * 'a list
--- a/src/Tools/Metis/src/Useful.sml Wed Sep 15 15:15:49 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml Wed Sep 15 15:44:24 2010 +0200
@@ -170,6 +170,10 @@
(* Lists. *)
(* ------------------------------------------------------------------------- *)
+val foldl = List.foldl; (* MODIFIED by Jasmin Blanchette *)
+
+val foldr = List.foldr; (* MODIFIED by Jasmin Blanchette *)
+
fun cons x y = x :: y;
fun hdTl l = (hd l, tl l);