1.1 --- a/src/Doc/IsarRef/Proof.thy	Tue Sep 03 11:55:59 2013 +0200
     1.2 +++ b/src/Doc/IsarRef/Proof.thy	Tue Sep 03 11:58:34 2013 +0200
     1.3 @@ -1195,7 +1195,7 @@
     1.4    later.
     1.5  
     1.6    @{rail "
     1.7 -    @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')')
     1.8 +    @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
     1.9      ;
    1.10      caseref: nameref attributes?
    1.11      ;

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 03 11:55:59 2013 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 03 11:58:34 2013 +0200
     2.3 @@ -608,14 +608,12 @@
     2.4      (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
     2.5      >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
     2.6  
     2.7 -val case_spec =
     2.8 -  (@{keyword "("} |--
     2.9 -    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
    2.10 -    Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
    2.11 -
    2.12  val _ =
    2.13    Outer_Syntax.command @{command_spec "case"} "invoke local context"
    2.14 -    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
    2.15 +    ((@{keyword "("} |--
    2.16 +      Parse.!!! (Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
    2.17 +      Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
    2.18 +        Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
    2.19  
    2.20  
    2.21  (* proof structure *)