src/Tools/Code/code_scala.ML
changeset 39059 3a11a667af75
parent 39058 551fe1af03b0
child 39102 4ae1d212100f
equal deleted inserted replaced
39058:551fe1af03b0 39059:3a11a667af75
   315          of Code_Thingol.Classinst _ => true
   315          of Code_Thingol.Classinst _ => true
   316           | _ => false;
   316           | _ => false;
   317         val implicits = filter (is_classinst o Graph.get_node program)
   317         val implicits = filter (is_classinst o Graph.get_node program)
   318           (Graph.imm_succs program name);
   318           (Graph.imm_succs program name);
   319       in union (op =) implicits end;
   319       in union (op =) implicits end;
   320     fun modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
   320     fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
       
   321       | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
   321       | modify_stmt (_, Code_Thingol.Classrel _) = NONE
   322       | modify_stmt (_, Code_Thingol.Classrel _) = NONE
   322       | modify_stmt (_, Code_Thingol.Classparam _) = NONE
   323       | modify_stmt (_, Code_Thingol.Classparam _) = NONE
   323       | modify_stmt (_, stmt) = SOME stmt;
   324       | modify_stmt (_, stmt) = SOME stmt;
   324   in
   325   in
   325     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   326     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,