# HG changeset patch
# User wenzelm
# Date 1006445616 -3600
# Node ID 50e2bca71c9d8c741e528924983c057160164851
# Parent  fa0a3e95d395513d9d288ca32a981ac9139c608d
tuned;

diff -r fa0a3e95d395 -r 50e2bca71c9d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 22 17:13:24 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 22 17:13:36 2001 +0100
@@ -385,8 +385,8 @@
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
 
 val case_spec =
-  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.underscore >> K None || P.name >> Some)
-    --| P.$$$ ")") || P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
+  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 P.uname --| P.$$$ ")") ||
+    P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
 
 val caseP =
   OuterSyntax.command "case" "invoke local context" K.prf_asm