# HG changeset patch
# User haftmann
# Date 1130770815 -3600
# Node ID 652c95961a8b8befa4a52637d128ab73d6b8d6c1
# Parent  156bba334c123ae06f78bcba934414fee5535666
fold_index replacing foldln

diff -r 156bba334c12 -r 652c95961a8b TFL/casesplit.ML
--- a/TFL/casesplit.ML	Mon Oct 31 01:43:22 2005 +0100
+++ b/TFL/casesplit.ML	Mon Oct 31 16:00:15 2005 +0100
@@ -336,31 +336,24 @@
 
 (* derive eqs, assuming strict, ie the rules have no assumptions = all
    the well-foundness conditions have been solved. *)
-local
-  fun get_related_thms i =
-      List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
-
-  fun solve_eq (th, [], i) =
-      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
-    | solve_eq (th, [a], i) = (a, i)
-    | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i);
-in
 fun derive_init_eqs sgn rules eqs =
-    let
-      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop)
-                      eqs
-    in
-      (rev o map solve_eq)
-        (Library.foldln
-           (fn (e,i) =>
-               (curry (op ::)) (e, (get_related_thms (i - 1) rules), i - 1))
-           eqths [])
-    end;
-end;
-(*
-    val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules)
-    (map2 (op |>) (ths, expfs))
-*)
+  let
+    fun get_related_thms i =
+      List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
+    fun add_eq (i, e) xs =
+      (e, (get_related_thms i rules), i) :: xs
+    fun solve_eq (th, [], i) =
+          raise ERROR_MESSAGE "derive_init_eqs: missing rules"
+      | solve_eq (th, [a], i) = (a, i)
+      | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
+    val eqths =
+      map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs;
+  in
+    []
+    |> fold_index add_eq eqths 
+    |> map solve_eq
+    |> rev
+  end;
 
 end;
 
diff -r 156bba334c12 -r 652c95961a8b src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Mon Oct 31 01:43:22 2005 +0100
+++ b/src/HOL/Tools/split_rule.ML	Mon Oct 31 16:00:15 2005 +0100
@@ -120,14 +120,16 @@
 
 fun split_rule_goal xss rl =
   let
-    fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
-    fun one_goal (xs, i) th = Library.foldl (one_split i) (th, xs);
+    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
+    fun one_goal (i, xs) = fold (one_split (i+1)) xs;
   in
-    Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
+    rl
+    |> Library.fold_index one_goal xss
+    |> Simplifier.full_simplify split_rule_ss
+    |> Drule.standard 
     |> RuleCases.save rl
   end;
 
-
 (* attribute syntax *)
 
 (* FIXME dynamically scoped due to Args.name/pair_tac *)
diff -r 156bba334c12 -r 652c95961a8b src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Mon Oct 31 01:43:22 2005 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Mon Oct 31 16:00:15 2005 +0100
@@ -142,7 +142,9 @@
 
 (* params *)
 
-fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
+fun rename_params xss thm =
+  thm
+  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i+1)) xss
   |> save thm;
 
 fun params xss = Drule.rule_attribute (K (rename_params xss));
diff -r 156bba334c12 -r 652c95961a8b src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Oct 31 01:43:22 2005 +0100
+++ b/src/Pure/library.ML	Mon Oct 31 16:00:15 2005 +0100
@@ -99,7 +99,7 @@
   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
-  val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
+  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val unflat: 'a list list -> 'b list -> 'b list list
   val splitAt: int * 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
@@ -504,7 +504,11 @@
         | itr (x::l) = f(x, itr l)
   in  itr l  end;
 
-fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
+fun fold_index f =
+  let
+    fun fold_aux _  [] y = y
+      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
+  in fold_aux 0 end;
 
 fun foldl_map f =
   let