moved ML syntax operations to structure ML_Syntax;

--- 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]);