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;