# HG changeset patch
# User wenzelm
# Date 1138894298 -3600
# Node ID f1333b0ff9e53d0b5863ccc0d53551803c4026ba
# Parent  fb080097e4366a375cdfde92aec7374147594b81
consumes: negative argument relative to total number of prems;

diff -r fb080097e436 -r f1333b0ff9e5 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Feb 02 16:31:37 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Feb 02 16:31:38 2006 +0100
@@ -226,7 +226,8 @@
 fun put_consumes NONE th = th
   | put_consumes (SOME n) th = th
       |> PureThy.untag_rule consumes_tagN
-      |> PureThy.tag_rule (consumes_tagN, [Library.string_of_int n]);
+      |> PureThy.tag_rule
+        (consumes_tagN, [Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n)]);
 
 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;