--- 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