diff -r e29ea98a76ce -r 3450e57264b3 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Feb 01 21:09:52 2011 +0100 +++ b/src/Tools/Code/code_scala.ML Wed Feb 02 10:34:14 2011 +0100 @@ -103,7 +103,9 @@ and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); - fun print_match ((IVar NONE, _), t) vars = + fun print_match ((IVar NONE, _), t as _ `|=> _) vars = + ((false, enclose "{" "}" [print_term tyvars false some_thm vars NOBR t]), vars) + | print_match ((IVar NONE, _), t) vars = ((true, print_term tyvars false some_thm vars NOBR t), vars) | print_match ((pat, ty), t) vars = vars