# HG changeset patch
# User haftmann
# Date 1283416190 -7200
# Node ID 2bb34f36db808fb0ef5ad1390a8225727bcca579
# Parent  cef7b58555aad318feb864feac6f4a5c2857487f
include names need not be considered as reserved any longer

diff -r cef7b58555aa -r 2bb34f36db80 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Sep 02 10:29:49 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 10:29:50 2010 +0200
@@ -333,9 +333,8 @@
   let
 
     (* build program *)
-    val reserved = fold (insert (op =) o fst) includes reserved_syms;
     val { deresolver, hierarchical_program = sca_program } =
-      scala_program_of_program labelled_name (Name.make_context reserved) module_alias program;
+      scala_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
 
     (* print statements *)
     fun lookup_constr tyco constr = case Graph.get_node program tyco
@@ -355,7 +354,7 @@
      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
-      (make_vars reserved) args_num is_singleton_constr;
+      (make_vars reserved_syms) args_num is_singleton_constr;
 
     (* print nodes *)
     fun print_module base implicit_ps p = Pretty.chunks2