# HG changeset patch
# User wenzelm
# Date 1015018358 -3600
# Node ID 3d5807d4543927261ba7ad871684251a7b7bf301
# Parent  e844d0ee15d51ed0cd89fcff924cd844df52e227
clarified outer syntax;

diff -r e844d0ee15d5 -r 3d5807d45439 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Mar 01 22:32:10 2002 +0100
+++ b/src/Pure/codegen.ML	Fri Mar 01 22:32:38 2002 +0100
@@ -470,7 +470,7 @@
   OuterSyntax.command "consts_code"
   "associate constants with target language code" K.thy_decl
     (Scan.repeat1
-       (P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --|
+       (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
         P.$$$ "(" -- P.string --| P.$$$ ")") >>
      (fn xs => Toplevel.theory (fn thy => assoc_consts
        (map (fn ((name, optype), mfx) => (name, optype, parse_mixfix
@@ -479,8 +479,8 @@
 
 val generate_codeP =
   OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
-    (Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") --
-     Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >>
+    (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+     Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) >>
      (fn (opt_fname, xs) => Toplevel.theory (fn thy =>
         ((case opt_fname of
             None => use_text Context.ml_output false