consume: unfold defs in all major prems;

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