# HG changeset patch
# User blanchet
# Date 1284558264 -7200
# Node ID 782477d78f63fa3b8b8d55bb4558d4923a177e9a
# Parent  65a379f4c8f32d6d0b7765a76d03040a9cfb268c
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

diff -r 65a379f4c8f3 -r 782477d78f63 src/Tools/Metis/src/Useful.sig
--- 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
diff -r 65a379f4c8f3 -r 782477d78f63 src/Tools/Metis/src/Useful.sml
--- 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);