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