dropped redundancy
authorhaftmann
Sat, 19 Feb 2011 08:47:46 +0100
changeset 41784 537013b8ba8e
parent 41783 717b8ffa1a16
child 41785 77dcc197df9a
dropped redundancy
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) =