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