1.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Oct 05 22:00:15 2007 +0200
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Oct 05 22:00:17 2007 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4    val consume: thm list -> thm list -> ('a * int) * thm ->
     1.5      (('a * (int * thm list)) * thm) Seq.seq
     1.6    val add_consumes: int -> thm -> thm
     1.7 +  val get_consumes: thm -> int
     1.8    val consumes: int -> attribute
     1.9    val consumes_default: int -> attribute
    1.10    val name: string list -> thm -> thm