# HG changeset patch
# User wenzelm
# Date 1132941523 -3600
# Node ID 8de262a22f23cf7bae6615d8b28a2302bf60a7bf
# Parent  5ef79b75a002b1c9702a482eaecb200d9d1d98a2
consume: unfold defs in all major prems;

diff -r 5ef79b75a002 -r 8de262a22f23 src/Pure/Isar/rule_cases.ML
--- 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";