1.1 --- a/src/HOL/Tools/split_rule.ML	Mon Oct 31 01:43:22 2005 +0100
     1.2 +++ b/src/HOL/Tools/split_rule.ML	Mon Oct 31 16:00:15 2005 +0100
     1.3 @@ -120,14 +120,16 @@
     1.4  
     1.5  fun split_rule_goal xss rl =
     1.6    let
     1.7 -    fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
     1.8 -    fun one_goal (xs, i) th = Library.foldl (one_split i) (th, xs);
     1.9 +    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
    1.10 +    fun one_goal (i, xs) = fold (one_split (i+1)) xs;
    1.11    in
    1.12 -    Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
    1.13 +    rl
    1.14 +    |> Library.fold_index one_goal xss
    1.15 +    |> Simplifier.full_simplify split_rule_ss
    1.16 +    |> Drule.standard 
    1.17      |> RuleCases.save rl
    1.18    end;
    1.19  
    1.20 -
    1.21  (* attribute syntax *)
    1.22  
    1.23  (* FIXME dynamically scoped due to Args.name/pair_tac *)