Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified outer syntax;
authorwenzelm
Fri, 01 Mar 2002 22:32:38 +0100
changeset 13003 3d5807d45439
parent 13002 e844d0ee15d5
child 13004 7c3d4e57e3d4
clarified outer syntax;
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle