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.
Quoted terms in consts_code declarations are now preprocessed as well.
authorberghofe
Mon, 04 Aug 2008 18:57:35 +0200
changeset 27724 0cc30a837f26
parent 27723 ce8f79b91ed1
child 27725 6d133c2b681f
Quoted terms in consts_code declarations are now preprocessed as well.
src/Pure/codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/codegen.ML	Mon Aug 04 18:56:55 2008 +0200
+++ b/src/Pure/codegen.ML	Mon Aug 04 18:57:35 2008 +0200
@@ -681,7 +681,8 @@
                  val (ts1, ts2) = args_of ms ts;
                  val (gr1, ps1) = codegens false (gr, ts1);
                  val (gr2, ps2) = codegens true (gr1, ts2);
-                 val (gr3, ps3) = codegens false (gr2, quotes_of ms);
+                 val (gr3, ps3) = codegens false (gr2,
+                   map (preprocess_term thy) (quotes_of ms));
                  val (gr4, _) = invoke_tycodegen thy defs dep module false
                    (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
                  val (module', suffix) = (case get_defn thy defs s T of
isabelle