--- a/src/HOL/HOL.thy Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/HOL.thy Tue Mar 22 20:44:47 2011 +0100
@@ -106,7 +106,7 @@
iff (infixr "\<longleftrightarrow>" 25)
nonterminal letbinds and letbind
-nonterminal case_syn and cases_syn
+nonterminal case_pat and case_syn and cases_syn
syntax
"_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10)
@@ -116,10 +116,14 @@
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10)
- "_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
- "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
- "" :: "case_syn => cases_syn" ("_")
- "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
+ "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
+ "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ =>/ _)" 10)
+ "" :: "case_syn => cases_syn" ("_")
+ "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
+ "_strip_positions" :: "'a => case_pat" ("_")
+
+syntax (xsymbols)
+ "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
translations
"THE x. P" == "CONST The (%x. P)"
@@ -130,9 +134,6 @@
in Syntax.const @{syntax_const "_The"} $ x $ t end)]
*} -- {* To avoid eta-contraction of body *}
-syntax (xsymbols)
- "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10)
-
notation (xsymbols)
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and