# HG changeset patch
# User wenzelm
# Date 952555714 -3600
# Node ID 2dd4823c744f0dae11565fe825e18a50718011ad
# Parent  52d5fae273dd9ddaebf5ce4038e8fe0aa72492ad
invoke_case: name assumption;

diff -r 52d5fae273dd -r 2dd4823c744f 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;