src/HOL/Sum.thy

--- a/src/HOL/Sum.thy	Fri Apr 18 11:47:36 1997 +0200
+++ b/src/HOL/Sum.thy	Fri Apr 18 11:48:16 1997 +0200
@@ -34,7 +34,7 @@
   Part          :: ['a set, 'b => 'a] => 'a set
 
 translations
-  "case p of Inl(x) => a | Inr(y) => b" == "sum_case (%x.a) (%y.b) p"
+  "case p of Inl x => a | Inr y => b" == "sum_case (%x.a) (%y.b) p"
 
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"