--- 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));
--- 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 *)