invoke_case: name assumption;
authorwenzelm
Wed Mar 08 23:48:34 2000 +0100 (2000-03-08)
changeset 83832dd4823c744f
parent 8382 52d5fae273dd
child 8384 13bc74731ae6
invoke_case: name assumption;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 08 23:47:44 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 08 23:48:34 2000 +0100
     1.3 @@ -565,7 +565,7 @@
     1.4    let val (vars, props) = get_case state name in
     1.5      state
     1.6      |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
     1.7 -    |> assume_i [("", [], map (fn t => (t, ([], []))) props)]
     1.8 +    |> assume_i [(name, [], map (fn t => (t, ([], []))) props)]
     1.9    end;
    1.10  
    1.11