--- a/src/Pure/Tools/codegen_serializer.ML Thu Nov 23 00:52:01 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Thu Nov 23 00:52:03 2006 +0100
@@ -567,7 +567,8 @@
datatype node =
Def of string * ml_def option
| Module of string * ((Name.context * Name.context) * node Graph.T);
- val empty_names = Name.make_context ("nil" :: ThmDatabase.ml_reserved @ reserved_user);
+ val empty_names =
+ Name.make_context ("nil" :: (* FIXME !? *) ML_Syntax.reserved @ reserved_user);
val empty_module = ((empty_names, empty_names), Graph.empty);
fun map_node [] f = f
| map_node (m::ms) f =
@@ -587,7 +588,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 (ThmDatabase.ml_reserved @ reserved_user);
+ val init_vars = CodegenThingol.make_vars (ML_Syntax.reserved @ reserved_user);
fun name_modl modl =
let
val modlname = NameSpace.pack modl