# HG changeset patch
# User paulson
# Date 861356896 -7200
# Node ID f914a1663b2ac5502aea6bbf89ce242d47664066
# Parent  85c81d524655635276ff67d18c35b5f62843fcc0
Removed needless parentheses from translation

diff -r 85c81d524655 -r f914a1663b2a 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)))"