diff -r e654599b114e -r ad2f5da643b4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/HOL.thy	Mon Jan 26 10:34:02 2004 +0100
@@ -96,7 +96,7 @@
   "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
-(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
+(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
 
 syntax (xsymbols output)
   "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)