# HG changeset patch
# User wenzelm
# Date 999296444 -7200
# Node ID 2b3f02227c356c49f2e5f2f00a005a2347963b30
# Parent  0b56d9c90dcf7e7ec6fb18e97a92ca93a4a9749d
tuned;

diff -r 0b56d9c90dcf -r 2b3f02227c35 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Sat Sep 01 00:20:22 2001 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Sat Sep 01 00:20:44 2001 +0200
@@ -311,7 +311,7 @@
     SynExt {
       logtypes = logtypes',
       xprods = xprods,
-      consts = consts union mfix_consts,
+      consts = consts union_string mfix_consts,
       prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
       parse_ast_translation = parse_ast_translation,
       parse_rules = parse_rules,
diff -r 0b56d9c90dcf -r 2b3f02227c35 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Sep 01 00:20:22 2001 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Sep 01 00:20:44 2001 +0200
@@ -209,7 +209,7 @@
       logtypes = extend_list logtypes1 logtypes2,
       gram = if inout then Parser.extend_gram gram xprods else gram,
       consts = consts2 @ consts1,
-      prmodes = (mode ins prmodes2) union_string prmodes1,
+      prmodes = (mode ins_string prmodes2) union_string prmodes1,
       parse_ast_trtab =
         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
       parse_ruletab = extend_ruletab parse_ruletab parse_rules,
diff -r 0b56d9c90dcf -r 2b3f02227c35 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Sep 01 00:20:22 2001 +0200
+++ b/src/Pure/codegen.ML	Sat Sep 01 00:20:44 2001 +0200
@@ -151,7 +151,7 @@
   end) (thy, xs);
 
 fun get_assoc_types thy = #types (CodegenData.get thy);
-         
+
 
 (**** retrieve definition of constant ****)
 
@@ -377,19 +377,17 @@
      (p, []) => p
    | _ => error ("Malformed annotation: " ^ quote s));
 
-structure P = OuterParse;
+structure P = OuterParse and K = OuterSyntax.Keyword;
 
 val assoc_typeP =
   OuterSyntax.command "types_code"
-  "associate types with target language types"
-  OuterSyntax.Keyword.thy_decl
+  "associate types with target language types" K.thy_decl
     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
      (Toplevel.theory o assoc_types));
 
 val assoc_constP =
   OuterSyntax.command "consts_code"
-  "associate constants with target language code"
-  OuterSyntax.Keyword.thy_decl
+  "associate constants with target language code" K.thy_decl
     (Scan.repeat1
        (P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --|
         P.$$$ "(" -- P.string --| P.$$$ ")") >>
@@ -399,10 +397,9 @@
            xs) thy)));
 
 val generate_codeP =
-  OuterSyntax.command "generate_code" "generates code for terms"
-  OuterSyntax.Keyword.thy_decl
+  OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
     (Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") --
-     Scan.repeat1 (P.short_ident --| P.$$$ "=" -- P.string) >>
+     Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >>
      (fn (opt_fname, xs) => Toplevel.theory (fn thy =>
         ((case opt_fname of
             None => use_text Context.ml_output false