src/Pure/Isar/proof.ML
changeset 8450 dc44d6533f0f
parent 8383 2dd4823c744f
child 8462 7f4e4e875c13
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Mar 14 11:32:38 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Mar 14 11:33:14 2000 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4      -> state -> state
     1.5    val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
     1.6      -> state -> state
     1.7 -  val invoke_case: string -> state -> state
     1.8 +  val invoke_case: string * context attribute list -> state -> state
     1.9    val theorem: bstring -> theory attribute list -> string * (string list * string list)
    1.10      -> theory -> state
    1.11    val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
    1.12 @@ -561,11 +561,11 @@
    1.13  
    1.14  (* invoke_case *)
    1.15  
    1.16 -fun invoke_case name state =
    1.17 +fun invoke_case (name, atts) state =
    1.18    let val (vars, props) = get_case state name in
    1.19      state
    1.20      |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
    1.21 -    |> assume_i [(name, [], map (fn t => (t, ([], []))) props)]
    1.22 +    |> assume_i [(name, atts, map (fn t => (t, ([], []))) props)]
    1.23    end;
    1.24  
    1.25