# HG changeset patch
# User oheimb
# Date 980877226 -3600
# Node ID e33dfe9bde39849b1d3ab63f86920403782e7bb9
# Parent  6754fa0f2af72cae6e116de0d46b5bcd638eb26c
added foldln

diff -r 6754fa0f2af7 -r e33dfe9bde39 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Jan 30 18:48:33 2001 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Tue Jan 30 18:53:46 2001 +0100
@@ -104,8 +104,7 @@
 
 (* params *)
 
-fun rename_params xss thm =
-  #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss))
+fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
   |> save thm;
 
 fun params xss = Drule.rule_attribute (K (rename_params xss));
diff -r 6754fa0f2af7 -r e33dfe9bde39 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jan 30 18:48:33 2001 +0100
+++ b/src/Pure/library.ML	Tue Jan 30 18:53:46 2001 +0100
@@ -85,6 +85,7 @@
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
+  val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val length: 'a list -> int
   val take: int * 'a list -> 'a list
   val drop: int * 'a list -> 'a list
@@ -477,6 +478,7 @@
         val (x'', ys') = foldl_map f (x', ys);
       in (x'', y' :: ys') end;
 
+fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
 
 (* basic list functions *)