# HG changeset patch
# User wenzelm
# Date 1165683938 -3600
# Node ID b67fbfc8a126acfd828461389461543c9639c495
# Parent  43b935d6fb5a726c3915418b3372be8e7c769cec
ML_Syntax.reserved(_names);

diff -r 43b935d6fb5a -r b67fbfc8a126 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Sat Dec 09 18:05:37 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Sat Dec 09 18:05:38 2006 +0100
@@ -567,7 +567,7 @@
     datatype node =
         Def of string * ml_def option
       | Module of string * ((Name.context * Name.context) * node Graph.T);
-    val empty_names = Name.make_context ("o" :: ML_Syntax.reserved @ reserved_user);
+    val empty_names = ML_Syntax.reserved |> fold Name.declare ("o" :: reserved_user);
     val empty_module = ((empty_names, empty_names), Graph.empty);
     fun map_node [] f = f
       | map_node (m::ms) f =
@@ -587,7 +587,7 @@
                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
                   in (x, Module (dmodlname, nsp_nodes')) end)
           in (x, (nsp, nodes')) end;
-    val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved @ reserved_user);
+    val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved_names @ reserved_user);
     fun name_modl modl =
       let
         val modlname = NameSpace.pack modl
diff -r 43b935d6fb5a -r b67fbfc8a126 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Dec 09 18:05:37 2006 +0100
+++ b/src/Pure/codegen.ML	Sat Dec 09 18:05:38 2006 +0100
@@ -689,7 +689,7 @@
 
 fun new_names t xs = Name.variant_list
   (map (fst o fst o dest_Var) (term_vars t) union
-    add_term_names (t, ML_Syntax.reserved)) (map mk_id xs);
+    add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
 
 fun new_name t x = hd (new_names t [x]);