# HG changeset patch
# User krauss
# Date 1192536695 -7200
# Node ID 3d0137a59dcb140c0c10d7bcb6c59a09859f11e1
# Parent  12386aefe9aca40ae790bd945e7286dcdfa62c44
Fixed variable naming in mutual induction rules

diff -r 12386aefe9ac -r 3d0137a59dcb src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Oct 16 14:11:06 2007 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Oct 16 14:11:35 2007 +0200
@@ -286,18 +286,19 @@
                       |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
                       |> full_simplify (HOL_basic_ss addsimps all_f_defs)
           
-      fun project rule (MutualPart {cargTs, i, ...}) =
+      fun project rule (MutualPart {cargTs, i, ...}) k =
           let
-            val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int j, T)) cargTs
+            val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
             val inj = mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
           in
-            rule
+            (rule
               |> forall_elim (cert inj)
               |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
-              |> fold_rev (forall_intr o cert) (afs @ newPs)
+              |> fold_rev (forall_intr o cert) (afs @ newPs),
+             k + length cargTs)
           end
     in
-      map (project induct_inst) parts
+      fst (fold_map (project induct_inst) parts 0)
     end