# HG changeset patch
# User haftmann
# Date 1298101666 -3600
# Node ID 537013b8ba8e3c7b9070079beaa688423aaf1fdb
# Parent  717b8ffa1a167283dfb0bf203147915d9bbe34d7
dropped redundancy

diff -r 717b8ffa1a16 -r 537013b8ba8e src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sat Feb 19 08:39:05 2011 +0100
+++ b/src/Tools/Code/code_scala.ML	Sat Feb 19 08:47:46 2011 +0100
@@ -103,8 +103,6 @@
     and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
-            fun is_IAbs (_ `|=> _) = true
-              | is_IAbs _ = false;
             fun print_match_val ((pat, ty), t) vars =
               vars
               |> print_bind tyvars some_thm BR pat
@@ -113,7 +111,7 @@
             fun print_match_seq t vars =
               ((true, print_term tyvars false some_thm vars NOBR t), vars);
             fun print_match is_first ((IVar NONE, ty), t) =
-                  if is_IAbs t andalso is_first
+                  if Code_Thingol.is_IAbs t andalso is_first
                     then print_match_val ((IVar NONE, ty), t)
                     else print_match_seq t
               | print_match _ ((pat, ty), t) =