Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 22 Nov 2001 17:13:36 +0100
changeset 12267 50e2bca71c9d
parent 12266 fa0a3e95d395
child 12268 28e60c998eee
tuned;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle