# HG changeset patch
# User bulwahn
# Date 1296639341 -3600
# Node ID f9ff311992b6dae7f9cee08114fe47e2c7104c21
# Parent  d8efc2490b8e3ffac062879fc07322eb6d2941b9# Parent  3450e57264b362575ceae684f80675a19f82e9b1
merged

diff -r d8efc2490b8e -r f9ff311992b6 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Feb 02 08:47:45 2011 +0100
+++ b/src/Tools/Code/code_scala.ML	Wed Feb 02 10:35:41 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