# HG changeset patch
# User wenzelm
# Date 975370180 -3600
# Node ID 7934b0fa8dccd05e157882d17a47d6fd625fb36f
# Parent  ced4f4ec917e9a8da104f704cc88221c5062f7a2
consume facts;

diff -r ced4f4ec917e -r 7934b0fa8dcc src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Tue Nov 28 01:09:13 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Tue Nov 28 01:09:40 2000 +0100
@@ -158,8 +158,8 @@
 
     val cond_simp = if simplified then simplified_cases ctxt else rpair;
 
-    fun prep_rule (thm, cases) =
-      Seq.map (cond_simp cases) (Method.multi_resolves facts [thm]);
+    fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o cond_simp cases)
+      (Method.multi_resolves (take (n, facts)) [thm]);
   in
     Method.resolveq_cases_tac (RuleCases.make open_parms)
       (Seq.flat (Seq.map prep_rule (Seq.of_list rules)))
@@ -275,8 +275,8 @@
       | (([], Some thm), _) => [RuleCases.add thm]
       | ((insts, Some thm), _) => [(inst_rule insts thm, RuleCases.get thm)]);
 
-    fun prep_rule (thm, cases) =
-      Seq.map (rpair cases) (Method.multi_resolves facts [thm]);
+    fun prep_rule (thm, (cases, n)) =
+      Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]);
     val tac = Method.resolveq_cases_tac (rulify_cases cert open_parms)
       (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   in