# HG changeset patch
# User wenzelm
# Date 1180905410 -7200
# Node ID daca4731942f6e3e5e41ec0ab7ad30fe7fa29232
# Parent  f032bdc3eff48da4df40768c5f8700c46c254e8a
added downto0 (from library.ML);

diff -r f032bdc3eff4 -r daca4731942f src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Sun Jun 03 23:16:49 2007 +0200
+++ b/src/Pure/pattern.ML	Sun Jun 03 23:16:50 2007 +0200
@@ -151,7 +151,11 @@
   in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
 
 
-(* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
+(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
+fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
+  | downto0 ([], n) = n = ~1;
+
+(*mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ]*)
 fun mk_proj_list is =
     let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
           | mk([],_)    = []