# HG changeset patch
# User wenzelm
# Date 1378202314 -7200
# Node ID 21693b7c8fbf6a2838bae513d660a077b818b4f3
# Parent  1d4a46f1fced93d64fe8da2bf1665e956d0f0777
more liberal 'case' syntax: allow parentheses without arguments;

diff -r 1d4a46f1fced -r 21693b7c8fbf src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Tue Sep 03 11:55:59 2013 +0200
+++ b/src/Doc/IsarRef/Proof.thy	Tue Sep 03 11:58:34 2013 +0200
@@ -1195,7 +1195,7 @@
   later.
 
   @{rail "
-    @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) +) ')')
+    @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
     ;
     caseref: nameref attributes?
     ;
diff -r 1d4a46f1fced -r 21693b7c8fbf src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 03 11:55:59 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 03 11:58:34 2013 +0200
@@ -608,14 +608,12 @@
     (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
 
-val case_spec =
-  (@{keyword "("} |--
-    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
-    Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
-
 val _ =
   Outer_Syntax.command @{command_spec "case"} "invoke local context"
-    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
+    ((@{keyword "("} |--
+      Parse.!!! (Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
+      Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
+        Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
 
 
 (* proof structure *)