# HG changeset patch
# User haftmann
# Date 1283432991 -7200
# Node ID 3a11a667af757766b2bcc2e8dceedef176459b0f
# Parent  551fe1af03b00545e7e21b3c95791564ac4cc608
restored and added surpression of case combinators

diff -r 551fe1af03b0 -r 3a11a667af75 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 14:59:28 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 15:09:51 2010 +0200
@@ -759,10 +759,10 @@
     fun modify_class stmts = single (SOME
       (ML_Class (the_single (map_filter
         (fn (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
-    fun modify_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
-          [modify_fun stmt]
+    fun modify_stmts ([stmt as (name, stmt' as Code_Thingol.Fun _)]) =
+          if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
       | modify_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
-          modify_funs stmts
+          modify_funs (filter (Code_Thingol.is_case o snd) stmts)
       | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
           modify_datatypes stmts
       | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
diff -r 551fe1af03b0 -r 3a11a667af75 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Sep 02 14:59:28 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 15:09:51 2010 +0200
@@ -317,7 +317,8 @@
         val implicits = filter (is_classinst o Graph.get_node program)
           (Graph.imm_succs program name);
       in union (op =) implicits end;
-    fun modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
+    fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
+      | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
       | modify_stmt (_, Code_Thingol.Classrel _) = NONE
       | modify_stmt (_, Code_Thingol.Classparam _) = NONE
       | modify_stmt (_, stmt) = SOME stmt;