# HG changeset patch
# User krauss
# Date 1160481033 -7200
# Node ID f030835fd9e4db5cd01d99cb172268ba4d411c57
# Parent  9b9910b82645100cbd7525656e9d09c7092e67a7
Induction rules have schematic variables again.

diff -r 9b9910b82645 -r f030835fd9e4 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Tue Oct 10 12:08:12 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Tue Oct 10 13:50:33 2006 +0200
@@ -278,15 +278,20 @@
 
 fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
     let
-        fun mk_P (MutualPart {cargTs, ...}) Pname =
+      val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
+                                   Free (Pname, cargTs ---> HOLogic.boolT))
+                       (mutual_induct_Pnames (length parts))
+                       parts
+
+        fun mk_P (MutualPart {cargTs, ...}) P =
             let
                 val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
                 val atup = foldr1 HOLogic.mk_prod avars
             in
-                tupled_lambda atup (list_comb (Free (Pname, cargTs ---> HOLogic.boolT), avars))
+                tupled_lambda atup (list_comb (P, avars))
             end
 
-        val Ps = map2 mk_P parts (mutual_induct_Pnames (length parts))
+        val Ps = map2 mk_P parts newPs
         val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
 
         val induct_inst =
@@ -302,6 +307,7 @@
                 rule
                     |> forall_elim (cterm_of thy inj)
                     |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
+                    |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
             end
 
     in