--- 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
--- a/src/Pure/codegen.ML Thu Nov 23 00:52:01 2006 +0100
+++ b/src/Pure/codegen.ML Thu Nov 23 00:52:03 2006 +0100
@@ -477,7 +477,7 @@
let
val ((module, s), tab1') = mk_long_id tab1 module cname
val s' = mk_id s;
- val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_const" else s'
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
in ((gr, (tab1', tab2)), (module, s'')) end;
fun get_const_id cname (gr, (tab1, tab2)) =
@@ -486,14 +486,14 @@
| SOME (module, s) =>
let
val s' = mk_id s;
- val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_const" else s'
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
in (module, s'') end;
fun mk_type_id module tyname (gr, (tab1, tab2)) =
let
val ((module, s), tab2') = mk_long_id tab2 module tyname
val s' = mk_id s;
- val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_type" else s'
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
in ((gr, (tab1, tab2')), (module, s'')) end;
fun get_type_id tyname (gr, (tab1, tab2)) =
@@ -502,7 +502,7 @@
| SOME (module, s) =>
let
val s' = mk_id s;
- val s'' = if ThmDatabase.is_ml_reserved s' then s' ^ "_type" else s'
+ val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
in (module, s'') end;
fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab);
@@ -536,7 +536,7 @@
let
val names = foldr add_term_names
(map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
- val reserved = names inter ThmDatabase.ml_reserved;
+ val reserved = filter ML_Syntax.is_reserved names;
val (illegal, alt_names) = split_list (map_filter (fn s =>
let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
val ps = (reserved @ illegal) ~~
@@ -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, ThmDatabase.ml_reserved)) (map mk_id xs);
+ add_term_names (t, ML_Syntax.reserved)) (map mk_id xs);
fun new_name t x = hd (new_names t [x]);