# HG changeset patch
# User wenzelm
# Date 1357658587 -3600
# Node ID 6973b3f413340eb4952bd5c1e09ce0991f2b75c5
# Parent  2852f997bfb58f36e239cf9ae468a81b0e901b21
allow negative argument in "consumes" source format;
more documentation/NEWS;

diff -r 2852f997bfb5 -r 6973b3f41334 NEWS
--- a/NEWS	Tue Jan 08 16:01:07 2013 +0100
+++ b/NEWS	Tue Jan 08 16:23:07 2013 +0100
@@ -38,6 +38,13 @@
 specifications: nesting of "context fixes ... context assumes ..."
 and "class ... context ...".
 
+* Attribute "consumes" allows a negative value as well, which is
+interpreted relatively to the total number if premises of the rule in
+the target context.  This form of declaration is stable when exported
+from a nested 'context' with additional assumptions.  It is the
+preferred form for definitional packages, notably cases/rules produced
+in HOL/inductive and HOL/function.
+
 * More informative error messages for Isar proof commands involving
 lazy enumerations (method applications etc.).
 
diff -r 2852f997bfb5 -r 6973b3f41334 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Tue Jan 08 16:01:07 2013 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Tue Jan 08 16:23:07 2013 +0100
@@ -1197,7 +1197,7 @@
     ;
     @@{attribute params} ((@{syntax name} * ) + @'and')
     ;
-    @@{attribute consumes} @{syntax nat}?
+    @@{attribute consumes} @{syntax int}?
   "}
 
   \begin{description}
@@ -1245,7 +1245,15 @@
   \secref{sec:hol-inductive}).  Rules without any @{attribute
   consumes} declaration given are treated as if @{attribute
   consumes}~@{text 0} had been specified.
-  
+
+  A negative @{text n} is interpreted relatively to the total number
+  if premises of the rule in the target context.  Thus its absolute
+  value specifies the remaining number of premises, after subtracting
+  the prefix of major premises as indicated above. This form of
+  declaration has the technical advantage of being stable under more
+  morphisms, notably those that export the result from a nested
+  @{command_ref context} with additional assumptions.
+
   Note that explicit @{attribute consumes} declarations are only
   rarely needed; this is already taken care of automatically by the
   higher-level @{attribute cases}, @{attribute induct}, and
diff -r 2852f997bfb5 -r 6973b3f41334 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Jan 08 16:01:07 2013 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Jan 08 16:23:07 2013 +0100
@@ -391,7 +391,7 @@
     "rename bound variables in abstractions" #>
   setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
   setup (Binding.name "folded") folded "folded definitions" #>
-  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
+  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
     "number of consumed facts" #>
   setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
     "number of equality constraints" #>