# 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)))"