--- a/src/HOL/Bali/Basis.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Bali/Basis.thy Fri Apr 16 21:28:09 2010 +0200 @@ -176,7 +176,7 @@ section "sums" -hide const In0 In1 +hide_const In0 In1 notation sum_case (infixr "'(+')"80)