src/Pure/Tools/codegen_serializer.ML
changeset 21719 b67fbfc8a126
parent 21548 7c6216661e8a
child 21837 b8118942f0e2
--- 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