# HG changeset patch
# User traytel
# Date 1366794413 -7200
# Node ID cf039b3c42a73c05aef792b9653fa84f773c8137
# Parent  c27bb7994bd396882b0012896977132d147093ea
slightly more aggressive syntax translation for printing case expressions

diff -r c27bb7994bd3 -r cf039b3c42a7 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Apr 24 10:23:47 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 24 11:06:53 2013 +0200
@@ -156,7 +156,7 @@
 
 (* print translation *)
 
-fun case_tr' [_, x, t] =
+fun case_tr' (_ :: x :: t :: ts) =
       let
         fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
               let val (s', used') = Name.variant s used
@@ -171,9 +171,9 @@
               mk_clause t [] (Term.declare_term_frees t Name.context) ::
               mk_clauses u
       in
-        Syntax.const @{syntax_const "_case_syntax"} $ x $
+        list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $
           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
-            (mk_clauses t)
+            (mk_clauses t), ts)
       end;
 
 val trfun_setup' = Sign.add_trfuns