# HG changeset patch
# User wenzelm
# Date 1191614417 -7200
# Node ID 6b7258da912b2363706eeb45c75f33ef60cfcddc
# Parent  cc669ca5f38253556fbaec5502a898d18cf0a03d
export get_consumes;

diff -r cc669ca5f382 -r 6b7258da912b src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri Oct 05 22:00:15 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Fri Oct 05 22:00:17 2007 +0200
@@ -33,6 +33,7 @@
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
   val add_consumes: int -> thm -> thm
+  val get_consumes: thm -> int
   val consumes: int -> attribute
   val consumes_default: int -> attribute
   val name: string list -> thm -> thm