diff -r b640e50c91a1 -r 2131b6633529 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jul 02 08:03:50 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jul 02 12:12:26 2014 +0200
@@ -748,11 +748,11 @@
 
 local
 
-fun gen_invoke_case prep_att ((name, pos), xs, raw_atts) state =
+fun gen_invoke_case internal prep_att ((name, pos), xs, raw_atts) state =
   let
     val atts = map (prep_att (context_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
-      ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt (name, pos) xs));
+      ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs));
     val assumptions =
       asms |> map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts));
   in
@@ -764,8 +764,8 @@
 
 in
 
-val invoke_case = gen_invoke_case (K I);
-val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
+val invoke_case = gen_invoke_case true (K I);
+val invoke_case_cmd = gen_invoke_case false Attrib.attribute_cmd;
 
 end;