--- a/src/Pure/Isar/rule_cases.ML Fri Nov 25 18:58:42 2005 +0100
+++ b/src/Pure/Isar/rule_cases.ML Fri Nov 25 18:58:43 2005 +0100
@@ -66,12 +66,12 @@
(** consume facts **)
-fun consume defs facts ((x, n), th) =
+fun consume defs facts ((cases, n), th) =
let val m = Int.min (length facts, n) in
th |> K (not (null defs)) ?
- Drule.fconv_rule (Drule.goals_conv (fn i => i <= m) (Tactic.rewrite true defs))
+ Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs))
|> Drule.multi_resolve (Library.take (m, facts))
- |> Seq.map (pair (x, (n - m, Library.drop (m, facts))))
+ |> Seq.map (pair (cases, (n - m, Library.drop (m, facts))))
end;
val consumes_tagN = "consumes";