# HG changeset patch
# User haftmann
# Date 1164631361 -3600
# Node ID 7c6216661e8a2ff4d2a1c4886c7f8b2d432d1515
# Parent  9c9fdf4c2949bcf718d0be5ee0b77a6da64e1b3f
tuned keyword setup for SML code generator

diff -r 9c9fdf4c2949 -r 7c6216661e8a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 27 13:42:39 2006 +0100
+++ b/src/HOL/List.thy	Mon Nov 27 13:42:41 2006 +0100
@@ -2619,7 +2619,7 @@
   (Haskell infixl 4 "==")
 
 code_reserved SML
-  list char
+  list char nil
 
 code_reserved Haskell
   Char
diff -r 9c9fdf4c2949 -r 7c6216661e8a src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Mon Nov 27 13:42:39 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Nov 27 13:42:41 2006 +0100
@@ -567,8 +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 ("nil" :: (* FIXME !? *) ML_Syntax.reserved @ reserved_user);
+    val empty_names = Name.make_context ("o" :: ML_Syntax.reserved @ reserved_user);
     val empty_module = ((empty_names, empty_names), Graph.empty);
     fun map_node [] f = f
       | map_node (m::ms) f =
@@ -750,7 +749,7 @@
     fun output_internal p = use_text Output.ml_output false (Pretty.output p);
   in
     parse_args ((Args.$$$ "-" >> K output_diag
-      || Args.$$$ "*" >> K output_internal
+      || Args.$$$ "#" >> K output_internal
       || Args.name >> output_file)
     >> (fn output => seri_sml output))
   end;